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  1918  neorian  3050  2nreu  4402  tpprceq3  4767  tppreqb  4768  prneimg  4814  prneimg2  4815  prnebg  4816  preq12nebg  4823  opthprneg  4825  opthneg  5457  fr2nr  5632  iresn0n0  6050  xpeq0  6152  difxp  6156  ordtri3or  6390  imadif  6617  ftpg  7153  nf1const  7305  nf1oconst  7306  0mpo0  7496  2mpo0  7663  bropopvvv  8087  bropfvvvv  8089  frxp  8124  soxp  8127  ressuppssdif  8183  mpoxneldm  8210  naddcllem  8664  dfsup2  9414  nelaneqOLDOLD  9576  suc11reg  9598  rankxplim3  9863  kmlem3  10155  cdainflem  10190  isfin5-2  10393  mulge0b  12109  nn0n0n1ge2b  12597  rpneg  13076  mul2lt0bi  13150  xrrebnd  13220  xnn0xaddcl  13287  xmullem2  13317  difreicc  13537  fz0  13593  nelfzo  13720  injresinj  13847  hashunx  14450  swrdnd  14724  swrdnnn0nd  14726  swrdnd0  14727  repswswrd  14855  dfgcd2  16636  ncoprmlnprm  16819  firest  17517  xpcbas  18266  smndex2dnrinv  19027  symgfix2  19543  gsumdixp  20459  0ringnnzr  20686  isfieldidl  21449  mplsubrglem  22218  symgmatr01lem  22875  ppttop  23232  fin1aufil  24158  zclmncvs  25376  mbfmax  25877  mdegleb  26289  coemulhi  26480  noetasuplem4  27972  noetainflem4  27976  ltslpss  28173  lnssplng  29149  numedglnl  29601  usgredg2v  29687  clwwlkn  30496  clwwlkneq0  30499  clwwlknon1nloop  30569  trlsegvdeg  30707  1to2vfriswmgr  30759  numclwwlk3lem2  30864  atcvati  32867  difrab2  32973  ofpreima2  33139  hashxpe  33278  drnglring  33902  fldextrspunlsplem  34183  ordtconnlem1  34434  aean  34755  sitgaddlemb  34859  ballotlemodife  35009  bnj1174  35512  erdszelem10  35779  satfv1  35942  fmla0disjsuc  35977  fmlasucdisj  35978  dfon2lem4  36363  ltnadd  36798  naddle  36799  nrmo  37029  poimirlem30  38399  poimirlem31  38400  itg2addnclem  38420  itg2addnclem2  38421  itg2addnclem3  38422  iblabsnclem  38432  ftc1anclem3  38444  areacirclem4  38460  lsatcvat  39923  lkreqN  40043  cvrat  40295  4atlem3  40469  paddasslem17  40709  llnexchb2  40742  dalawlem14  40757  cdleme0nex  41163  lclkrlem2o  42394  lcfrlem19  42434  dvrelog2b  42932  aks4d1p7  42949  aks6d1c2p2  42985  aks6d1c5  43005  sticksstones1  43012  aks6d1c6lem3  43038  ifpnot23  44318  ifpim123g  44340  sqrtcvallem1  44471  ntrneineine1lem  44924  mnringmulrcld  45066  stoweidlem14  46842  stoweidlem26  46854  dfatprc  48018  afvco2  48064  ndmafv2nrn  48110  nfunsnafv2  48113  afv2ndeffv0  48148  nltle2tri  48201  ichnreuop  48372  spr0nelg  48376  evennodd  48559  oddneven  48560  usgrexmpl2trifr  48953  pg4cyclnex  49043  lindslinindsimp1  49387  lindslinindsimp2  49393  line2ylem  49681  line2xlem  49683