Theorem ianor 997

Description: Negated conjunction in terms of disjunction (De Morgan's law). Theorem *4.51 of [WhiteheadRussell] p. 120. (Contributed by NM, 14-May-1993.) (Proof shortened by Andrew Salmon, 13-May-2011.)

Assertion

Ref	Expression
ianor	⊢ (¬ (𝜑 ∧ 𝜓) ↔ (¬ 𝜑 ∨ ¬ 𝜓))

Proof of Theorem ianor

Step	Hyp	Ref	Expression
1		imnan 405	. 2 ⊢ ((𝜑 → ¬ 𝜓) ↔ ¬ (𝜑 ∧ 𝜓))
2		pm4.62 870	. 2 ⊢ ((𝜑 → ¬ 𝜓) ↔ (¬ 𝜑 ∨ ¬ 𝜓))
3	1, 2	bitr3i 280	1 ⊢ (¬ (𝜑 ∧ 𝜓) ↔ (¬ 𝜑 ∨ ¬ 𝜓))

This proof depends on syntax axioms:  ¬ wn 3   → wi 4   ↔ wb 209   ∧ wa 401   ∨ wo 861

This proof depends on axioms:  ax-mp 5  ax-1 6  ax-2 7  ax-3 8

This proof depends on definitions:  df-bi 210  df-an 402  df-or 862

This theorem is used by:  anor  998  3ianor  1124  nanor  1525  cadnot  1648  19.33b  1920  neorian  3054  2nreu  4405  tpprceq3  4769  tppreqb  4770  prneimg  4814  prneimg2  4815  prnebg  4816  preq12nebg  4823  opthprneg  4825  opthneg  5457  fr2nr  5635  iresn0n0  6064  xpeq0  6169  difxp  6173  ordtri3or  6421  imadif  6654  ftpg  7192  nf1const  7343  nf1oconst  7344  0mpo0  7534  2mpo0  7702  bropopvvv  8136  bropfvvvv  8138  frxp  8175  soxp  8178  ressuppssdif  8240  mpoxneldm  8267  naddcllem  8723  dfsup2  9473  nelaneqOLDOLD  9635  suc11reg  9657  rankxplim3  9935  kmlem3  10270  cdainflem  10305  isfin5-2  10508  mulge0b  12227  nn0n0n1ge2b  12715  rpneg  13194  mul2lt0bi  13268  xrrebnd  13338  xnn0xaddcl  13405  xmullem2  13435  difreicc  13655  fz0  13712  nelfzo  13839  injresinj  13966  hashunx  14571  swrdnd  14846  swrdnnn0nd  14848  swrdnd0  14849  repswswrd  14977  dfgcd2  16763  ncoprmlnprm  16948  firest  17653  xpcbas  18402  smndex2dnrinv  19164  symgfix2  19681  gsumdixp  20599  0ringnnzr  20827  isfieldidl  21591  mplsubrglem  22366  symgmatr01lem  23023  ppttop  23380  fin1aufil  24306  zclmncvs  25524  mbfmax  26025  mdegleb  26437  coemulhi  26628  noetasuplem4  28150  noetainflem4  28154  ltslpss  28351  lnssplng  29327  numedglnl  29779  usgredg2v  29865  clwwlkn  30674  clwwlkneq0  30677  clwwlknon1nloop  30747  trlsegvdeg  30885  1to2vfriswmgr  30937  numclwwlk3lem2  31042  atcvati  33045  difrab2  33193  ofpreima2  33358  hashxpe  33495  drnglring  34128  fldextrspunlsplem  34416  ordtconnlem1  34667  aean  34988  sitgaddlemb  35091  ballotlemodife  35241  bnj1174  35744  erdszelem10  36173  satfv1  36336  fmla0disjsuc  36371  fmlasucdisj  36372  mirimanoffr  36668  mirimanofffr  36670  dfon2lem4  36763  ltnadd  37182  naddle  37183  nrmo  37413  poimirlem30  38836  poimirlem31  38837  itg2addnclem  38857  itg2addnclem2  38858  itg2addnclem3  38859  iblabsnclem  38869  ftc1anclem3  38881  areacirclem4  38897  lsatcvat  40373  lkreqN  40493  cvrat  40745  4atlem3  40919  paddasslem17  41159  llnexchb2  41192  dalawlem14  41207  cdleme0nex  41613  lclkrlem2o  42844  lcfrlem19  42884  dvrelog2b  43382  aks4d1p7  43399  aks6d1c2p2  43435  aks6d1c5  43455  sticksstones1  43462  aks6d1c6lem3  43488  ifpnot23  44740  ifpim123g  44762  sqrtcvallem1  44892  ntrneineine1lem  45345  mnringmulrcld  45487  stoweidlem14  47297  stoweidlem26  47309  dfatprc  48473  afvco2  48519  ndmafv2nrn  48565  nfunsnafv2  48568  afv2ndeffv0  48603  nltle2tri  48656  ichnreuop  48827  spr0nelg  48831  evennodd  49014  oddneven  49015  usgrexmpl2trifr  49408  pg4cyclnex  49498  lindslinindsimp1  49900  lindslinindsimp2  49906  line2ylem  50194  line2xlem  50196