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  3055  2nreu  4409  tpprceq3  4774  tppreqb  4775  prneimg  4821  prneimg2  4822  prnebg  4823  preq12nebg  4830  opthprneg  4832  opthneg  5465  fr2nr  5640  iresn0n0  6058  xpeq0  6159  difxp  6163  ordtri3or  6397  imadif  6624  ftpg  7157  nf1const  7308  nf1oconst  7309  0mpo0  7499  2mpo0  7665  bropopvvv  8087  bropfvvvv  8089  frxp  8124  soxp  8127  ressuppssdif  8183  mpoxneldm  8210  naddcllem  8664  dfsup2  9407  nelaneqOLDOLD  9569  suc11reg  9591  rankxplim3  9856  kmlem3  10148  cdainflem  10183  isfin5-2  10386  mulge0b  12096  nn0n0n1ge2b  12584  rpneg  13062  mul2lt0bi  13136  xrrebnd  13206  xnn0xaddcl  13273  xmullem2  13303  difreicc  13523  fz0  13579  nelfzo  13706  injresinj  13833  hashunx  14436  swrdnd  14710  swrdnnn0nd  14712  swrdnd0  14713  repswswrd  14841  dfgcd2  16622  ncoprmlnprm  16805  firest  17503  xpcbas  18252  smndex2dnrinv  19001  symgfix2  19510  gsumdixp  20426  0ringnnzr  20653  isfieldidl  21416  mplsubrglem  22183  symgmatr01lem  22840  ppttop  23194  fin1aufil  24120  zclmncvs  25338  mbfmax  25839  mdegleb  26252  coemulhi  26442  noetasuplem4  27931  noetainflem4  27935  ltslpss  28132  lnssplng  29105  numedglnl  29525  usgredg2v  29611  clwwlkn  30420  clwwlkneq0  30423  clwwlknon1nloop  30493  trlsegvdeg  30625  1to2vfriswmgr  30677  numclwwlk3lem2  30782  atcvati  32785  difrab2  32891  ofpreima2  33058  hashxpe  33198  drnglring  33822  fldextrspunlsplem  34103  ordtconnlem1  34354  aean  34675  sitgaddlemb  34779  ballotlemodife  34929  bnj1174  35432  erdszelem10  35705  satfv1  35868  fmla0disjsuc  35903  fmlasucdisj  35904  dfon2lem4  36289  ltnadd  36723  naddle  36724  nrmo  36954  poimirlem30  38334  poimirlem31  38335  itg2addnclem  38355  itg2addnclem2  38356  itg2addnclem3  38357  iblabsnclem  38367  ftc1anclem3  38379  areacirclem4  38395  lsatcvat  39857  lkreqN  39977  cvrat  40229  4atlem3  40403  paddasslem17  40643  llnexchb2  40676  dalawlem14  40691  cdleme0nex  41097  lclkrlem2o  42328  lcfrlem19  42368  dvrelog2b  42866  aks4d1p7  42883  aks6d1c2p2  42919  aks6d1c5  42939  sticksstones1  42946  aks6d1c6lem3  42972  ifpnot23  44237  ifpim123g  44259  sqrtcvallem1  44390  ntrneineine1lem  44843  mnringmulrcld  44985  stoweidlem14  46761  stoweidlem26  46773  dfatprc  47900  afvco2  47946  ndmafv2nrn  47992  nfunsnafv2  47995  afv2ndeffv0  48030  nltle2tri  48083  ichnreuop  48254  spr0nelg  48258  evennodd  48441  oddneven  48442  usgrexmpl2trifr  48835  pg4cyclnex  48925  lindslinindsimp1  49270  lindslinindsimp2  49276  line2ylem  49564  line2xlem  49566