Theorem ianor 984

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 399	. 2 ⊢ ((𝜑 → ¬ 𝜓) ↔ ¬ (𝜑 ∧ 𝜓))
2		pm4.62 857	. 2 ⊢ ((𝜑 → ¬ 𝜓) ↔ (¬ 𝜑 ∨ ¬ 𝜓))
3	1, 2	bitr3i 277	1 ⊢ (¬ (𝜑 ∧ 𝜓) ↔ (¬ 𝜑 ∨ ¬ 𝜓))

Syntax hints:  ¬ wn 3   → wi 4   ↔ wb 206   ∧ wa 395   ∨ wo 848

This theorem was proved from axioms:  ax-mp 5  ax-1 6  ax-2 7  ax-3 8

This theorem depends on definitions:  df-bi 207  df-an 396  df-or 849

This theorem is referenced by:  anor  985  3ianor  1107  nanor  1497  cadnot  1617  19.33b  1887  neorian  3028  2nreu  4398  tpprceq3  4762  tppreqb  4763  prneimg  4812  prneimg2  4813  prnebg  4814  preq12nebg  4821  opthprneg  4823  opthneg  5437  fr2nr  5609  iresn0n0  6021  xpeq0  6126  difxp  6130  ordtri3or  6357  imadif  6584  ftpg  7111  nf1const  7260  nf1oconst  7261  0mpo0  7451  2mpo0  7617  bropopvvv  8042  bropfvvvv  8044  frxp  8078  soxp  8081  ressuppssdif  8137  mpoxneldm  8164  naddcllem  8614  dfsup2  9359  nelaneqOLD  9519  suc11reg  9540  rankxplim3  9805  kmlem3  10075  cdainflem  10110  isfin5-2  10313  mulge0b  12024  nn0n0n1ge2b  12482  rpneg  12951  mul2lt0bi  13025  xrrebnd  13095  xnn0xaddcl  13162  xmullem2  13192  difreicc  13412  fz0  13467  nelfzo  13592  injresinj  13719  hashunx  14321  swrdnd  14590  swrdnnn0nd  14592  swrdnd0  14593  repswswrd  14719  dfgcd2  16485  ncoprmlnprm  16667  firest  17364  xpcbas  18113  smndex2dnrinv  18852  symgfix2  19357  gsumdixp  20266  0ringnnzr  20470  mplsubrglem  21971  symgmatr01lem  22609  ppttop  22963  fin1aufil  23888  zclmncvs  25116  mbfmax  25618  mdegleb  26037  coemulhi  26227  noetasuplem4  27716  noetainflem4  27720  ltslpss  27916  numedglnl  29229  usgredg2v  29312  clwwlkn  30113  clwwlkneq0  30116  clwwlknon1nloop  30186  trlsegvdeg  30314  1to2vfriswmgr  30366  numclwwlk3lem2  30471  atcvati  32474  difrab2  32584  ofpreima2  32756  hashxpe  32898  fldextrspunlsplem  33851  ordtconnlem1  34102  aean  34422  sitgaddlemb  34526  ballotlemodife  34676  bnj1174  35179  erdszelem10  35416  satfv1  35579  fmla0disjsuc  35614  fmlasucdisj  35615  dfon2lem4  36000  nrmo  36626  poimirlem30  37901  poimirlem31  37902  itg2addnclem  37922  itg2addnclem2  37923  itg2addnclem3  37924  iblabsnclem  37934  ftc1anclem3  37946  areacirclem4  37962  lsatcvat  39426  lkreqN  39546  cvrat  39798  4atlem3  39972  paddasslem17  40212  llnexchb2  40245  dalawlem14  40260  cdleme0nex  40666  lclkrlem2o  41897  lcfrlem19  41937  dvrelog2b  42436  aks4d1p7  42453  aks6d1c2p2  42489  aks6d1c5  42509  sticksstones1  42516  aks6d1c6lem3  42542  ifpnot23  43834  ifpim123g  43856  sqrtcvallem1  43987  ntrneineine1lem  44440  mnringmulrcld  44584  stoweidlem14  46372  stoweidlem26  46384  dfatprc  47490  afvco2  47536  ndmafv2nrn  47582  nfunsnafv2  47585  afv2ndeffv0  47620  nltle2tri  47673  ichnreuop  47832  spr0nelg  47836  evennodd  48003  oddneven  48004  usgrexmpl2trifr  48397  pg4cyclnex  48487  lindslinindsimp1  48817  lindslinindsimp2  48823  line2ylem  49111  line2xlem  49113