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  3020  2nreu  4403  tpprceq3  4764  tppreqb  4765  prneimg  4814  prneimg2  4815  prnebg  4816  preq12nebg  4823  opthprneg  4825  opthneg  5436  fr2nr  5608  iresn0n0  6014  xpeq0  6121  difxp  6125  ordtri3or  6352  imadif  6584  ftpg  7110  nf1const  7261  nf1oconst  7262  0mpo0  7452  2mpo0  7618  bropopvvv  8046  bropfvvvv  8048  frxp  8082  soxp  8085  ressuppssdif  8141  mpoxneldm  8168  naddcllem  8617  dfsup2  9371  nelaneq  9528  suc11reg  9548  rankxplim3  9810  kmlem3  10082  cdainflem  10117  isfin5-2  10320  mulge0b  12029  nn0n0n1ge2b  12487  rpneg  12961  mul2lt0bi  13035  xrrebnd  13104  xnn0xaddcl  13171  xmullem2  13201  difreicc  13421  fz0  13476  nelfzo  13601  injresinj  13725  hashunx  14327  swrdnd  14595  swrdnnn0nd  14597  swrdnd0  14598  repswswrd  14725  dfgcd2  16492  ncoprmlnprm  16674  firest  17371  xpcbas  18115  smndex2dnrinv  18818  symgfix2  19322  gsumdixp  20204  0ringnnzr  20410  mplsubrglem  21889  symgmatr01lem  22516  ppttop  22870  fin1aufil  23795  zclmncvs  25024  mbfmax  25526  mdegleb  25945  coemulhi  26135  noetasuplem4  27624  noetainflem4  27628  sltlpss  27795  numedglnl  29047  usgredg2v  29130  clwwlkn  29928  clwwlkneq0  29931  clwwlknon1nloop  30001  trlsegvdeg  30129  1to2vfriswmgr  30181  numclwwlk3lem2  30286  atcvati  32288  difrab2  32400  ofpreima2  32563  hashxpe  32705  fldextrspunlsplem  33641  ordtconnlem1  33887  aean  34207  sitgaddlemb  34312  ballotlemodife  34462  bnj1174  34966  erdszelem10  35160  satfv1  35323  fmla0disjsuc  35358  fmlasucdisj  35359  dfon2lem4  35747  nrmo  36371  poimirlem30  37617  poimirlem31  37618  itg2addnclem  37638  itg2addnclem2  37639  itg2addnclem3  37640  iblabsnclem  37650  ftc1anclem3  37662  areacirclem4  37678  lsatcvat  39016  lkreqN  39136  cvrat  39389  4atlem3  39563  paddasslem17  39803  llnexchb2  39836  dalawlem14  39851  cdleme0nex  40257  lclkrlem2o  41488  lcfrlem19  41528  dvrelog2b  42027  aks4d1p7  42044  aks6d1c2p2  42080  aks6d1c5  42100  sticksstones1  42107  aks6d1c6lem3  42133  ifpnot23  43440  ifpim123g  43462  sqrtcvallem1  43593  ntrneineine1lem  44046  mnringmulrcld  44190  stoweidlem14  45985  stoweidlem26  45997  dfatprc  47104  afvco2  47150  ndmafv2nrn  47196  nfunsnafv2  47199  afv2ndeffv0  47234  nltle2tri  47287  ichnreuop  47446  spr0nelg  47450  evennodd  47617  oddneven  47618  usgrexmpl2trifr  48001  pg4cyclnex  48090  lindslinindsimp1  48419  lindslinindsimp2  48425  line2ylem  48713  line2xlem  48715