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  3027  2nreu  4384  tpprceq3  4749  tppreqb  4750  prneimg  4797  prneimg2  4798  prnebg  4799  preq12nebg  4806  opthprneg  4808  opthneg  5434  fr2nr  5608  iresn0n0  6019  xpeq0  6124  difxp  6128  ordtri3or  6355  imadif  6582  ftpg  7110  nf1const  7259  nf1oconst  7260  0mpo0  7450  2mpo0  7616  bropopvvv  8040  bropfvvvv  8042  frxp  8076  soxp  8079  ressuppssdif  8135  mpoxneldm  8162  naddcllem  8612  dfsup2  9357  nelaneqOLDOLD  9518  suc11reg  9540  rankxplim3  9805  kmlem3  10075  cdainflem  10110  isfin5-2  10313  mulge0b  12026  nn0n0n1ge2b  12506  rpneg  12976  mul2lt0bi  13050  xrrebnd  13120  xnn0xaddcl  13187  xmullem2  13217  difreicc  13437  fz0  13493  nelfzo  13619  injresinj  13746  hashunx  14348  swrdnd  14617  swrdnnn0nd  14619  swrdnd0  14620  repswswrd  14746  dfgcd2  16515  ncoprmlnprm  16698  firest  17395  xpcbas  18144  smndex2dnrinv  18886  symgfix2  19391  gsumdixp  20298  0ringnnzr  20502  mplsubrglem  21982  symgmatr01lem  22618  ppttop  22972  fin1aufil  23897  zclmncvs  25115  mbfmax  25616  mdegleb  26029  coemulhi  26219  noetasuplem4  27700  noetainflem4  27704  ltslpss  27900  numedglnl  29213  usgredg2v  29296  clwwlkn  30096  clwwlkneq0  30099  clwwlknon1nloop  30169  trlsegvdeg  30297  1to2vfriswmgr  30349  numclwwlk3lem2  30454  atcvati  32457  difrab2  32567  ofpreima2  32739  hashxpe  32880  fldextrspunlsplem  33817  ordtconnlem1  34068  aean  34388  sitgaddlemb  34492  ballotlemodife  34642  bnj1174  35145  erdszelem10  35382  satfv1  35545  fmla0disjsuc  35580  fmlasucdisj  35581  dfon2lem4  35966  nrmo  36592  poimirlem30  37971  poimirlem31  37972  itg2addnclem  37992  itg2addnclem2  37993  itg2addnclem3  37994  iblabsnclem  38004  ftc1anclem3  38016  areacirclem4  38032  lsatcvat  39496  lkreqN  39616  cvrat  39868  4atlem3  40042  paddasslem17  40282  llnexchb2  40315  dalawlem14  40330  cdleme0nex  40736  lclkrlem2o  41967  lcfrlem19  42007  dvrelog2b  42505  aks4d1p7  42522  aks6d1c2p2  42558  aks6d1c5  42578  sticksstones1  42585  aks6d1c6lem3  42611  ifpnot23  43905  ifpim123g  43927  sqrtcvallem1  44058  ntrneineine1lem  44511  mnringmulrcld  44655  stoweidlem14  46442  stoweidlem26  46454  dfatprc  47578  afvco2  47624  ndmafv2nrn  47670  nfunsnafv2  47673  afv2ndeffv0  47708  nltle2tri  47761  ichnreuop  47932  spr0nelg  47936  evennodd  48119  oddneven  48120  usgrexmpl2trifr  48513  pg4cyclnex  48603  lindslinindsimp1  48933  lindslinindsimp2  48939  line2ylem  49227  line2xlem  49229