Theorem ianor 981

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

Syntax hints:  ¬ wn 3   → wi 4   ↔ wb 209   ∧ wa 399   ∨ wo 846

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 210  df-an 400  df-or 847

This theorem is referenced by:  anor  982  3ianor  1108  nanor  1490  noranOLD  1532  cadnot  1621  19.33b  1892  neorian  3028  indifdirOLD  4176  2nreu  4331  tpprceq3  4692  tppreqb  4693  prneimg  4740  prnebg  4741  preq12nebg  4748  opthprneg  4750  opthneg  5339  fr2nr  5503  iresn0n0  5897  xpeq0  5992  difxp  5996  ordtri3or  6204  imadif  6423  ftpg  6930  nf1const  7073  nf1oconst  7074  0mpo0  7253  2mpo0  7412  bropopvvv  7813  bropfvvvv  7815  frxp  7848  soxp  7851  ressuppssdif  7882  mpoxneldm  7909  dfsup2  8983  nelaneq  9138  suc11reg  9157  rankxplim3  9385  kmlem3  9654  cdainflem  9689  isfin5-2  9893  mulge0b  11590  nn0n0n1ge2b  12046  rpneg  12506  mul2lt0bi  12580  xrrebnd  12646  xnn0xaddcl  12713  xmullem2  12743  difreicc  12960  fz0  13015  nelfzo  13136  injresinj  13251  hashunx  13841  swrdnd  14107  swrdnnn0nd  14109  swrdnd0  14110  repswswrd  14237  dfgcd2  15992  ncoprmlnprm  16170  firest  16811  xpcbas  17546  smndex2dnrinv  18198  symgfix2  18664  gsumdixp  19483  0ringnnzr  20163  mplsubrglem  20822  symgmatr01lem  21406  ppttop  21760  fin1aufil  22685  zclmncvs  23902  mbfmax  24403  mdegleb  24819  coemulhi  25005  numedglnl  27091  usgredg2v  27171  clwwlkn  27965  clwwlkneq0  27968  clwwlknon1nloop  28038  trlsegvdeg  28166  1to2vfriswmgr  28218  numclwwlk3lem2  28323  atcvati  30323  difrab2  30421  ofpreima2  30580  hashxpe  30704  ordtconnlem1  31448  aean  31784  sitgaddlemb  31887  ballotlemodife  32036  bnj1174  32556  erdszelem10  32735  satfv1  32898  fmla0disjsuc  32933  fmlasucdisj  32934  dfon2lem4  33338  naddcllem  33476  noetasuplem4  33584  noetainflem4  33588  sltlpss  33732  nrmo  34244  poimirlem30  35452  poimirlem31  35453  itg2addnclem  35473  itg2addnclem2  35474  itg2addnclem3  35475  iblabsnclem  35485  ftc1anclem3  35497  areacirclem4  35513  lsatcvat  36709  lkreqN  36829  cvrat  37081  4atlem3  37255  paddasslem17  37495  llnexchb2  37528  dalawlem14  37543  cdleme0nex  37949  lclkrlem2o  39180  lcfrlem19  39220  dvrelog2b  39715  sticksstones1  39730  ifpnot23  40661  ifpim123g  40683  sqrtcvallem1  40806  ntrneineine1lem  41262  mnringmulrcld  41410  stoweidlem14  43119  stoweidlem26  43131  dfatprc  44184  afvco2  44230  ndmafv2nrn  44276  nfunsnafv2  44279  afv2ndeffv0  44314  nltle2tri  44368  ichnreuop  44487  spr0nelg  44491  evennodd  44658  oddneven  44659  lindslinindsimp1  45361  lindslinindsimp2  45367  line2ylem  45660  line2xlem  45662