Theorem ianor 983

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

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

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 848

This theorem is referenced by:  anor  984  3ianor  1106  nanor  1495  cadnot  1615  19.33b  1885  neorian  3021  2nreu  4410  tpprceq3  4771  tppreqb  4772  prneimg  4821  prneimg2  4822  prnebg  4823  preq12nebg  4830  opthprneg  4832  opthneg  5444  fr2nr  5618  iresn0n0  6028  xpeq0  6136  difxp  6140  ordtri3or  6367  imadif  6603  ftpg  7131  nf1const  7282  nf1oconst  7283  0mpo0  7475  2mpo0  7641  bropopvvv  8072  bropfvvvv  8074  frxp  8108  soxp  8111  ressuppssdif  8167  mpoxneldm  8194  naddcllem  8643  dfsup2  9402  nelaneq  9559  suc11reg  9579  rankxplim3  9841  kmlem3  10113  cdainflem  10148  isfin5-2  10351  mulge0b  12060  nn0n0n1ge2b  12518  rpneg  12992  mul2lt0bi  13066  xrrebnd  13135  xnn0xaddcl  13202  xmullem2  13232  difreicc  13452  fz0  13507  nelfzo  13632  injresinj  13756  hashunx  14358  swrdnd  14626  swrdnnn0nd  14628  swrdnd0  14629  repswswrd  14756  dfgcd2  16523  ncoprmlnprm  16705  firest  17402  xpcbas  18146  smndex2dnrinv  18849  symgfix2  19353  gsumdixp  20235  0ringnnzr  20441  mplsubrglem  21920  symgmatr01lem  22547  ppttop  22901  fin1aufil  23826  zclmncvs  25055  mbfmax  25557  mdegleb  25976  coemulhi  26166  noetasuplem4  27655  noetainflem4  27659  sltlpss  27826  numedglnl  29078  usgredg2v  29161  clwwlkn  29962  clwwlkneq0  29965  clwwlknon1nloop  30035  trlsegvdeg  30163  1to2vfriswmgr  30215  numclwwlk3lem2  30320  atcvati  32322  difrab2  32434  ofpreima2  32597  hashxpe  32739  fldextrspunlsplem  33675  ordtconnlem1  33921  aean  34241  sitgaddlemb  34346  ballotlemodife  34496  bnj1174  35000  erdszelem10  35194  satfv1  35357  fmla0disjsuc  35392  fmlasucdisj  35393  dfon2lem4  35781  nrmo  36405  poimirlem30  37651  poimirlem31  37652  itg2addnclem  37672  itg2addnclem2  37673  itg2addnclem3  37674  iblabsnclem  37684  ftc1anclem3  37696  areacirclem4  37712  lsatcvat  39050  lkreqN  39170  cvrat  39423  4atlem3  39597  paddasslem17  39837  llnexchb2  39870  dalawlem14  39885  cdleme0nex  40291  lclkrlem2o  41522  lcfrlem19  41562  dvrelog2b  42061  aks4d1p7  42078  aks6d1c2p2  42114  aks6d1c5  42134  sticksstones1  42141  aks6d1c6lem3  42167  ifpnot23  43474  ifpim123g  43496  sqrtcvallem1  43627  ntrneineine1lem  44080  mnringmulrcld  44224  stoweidlem14  46019  stoweidlem26  46031  dfatprc  47135  afvco2  47181  ndmafv2nrn  47227  nfunsnafv2  47230  afv2ndeffv0  47265  nltle2tri  47318  ichnreuop  47477  spr0nelg  47481  evennodd  47648  oddneven  47649  usgrexmpl2trifr  48032  pg4cyclnex  48121  lindslinindsimp1  48450  lindslinindsimp2  48456  line2ylem  48744  line2xlem  48746