Theorem ianor 978

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

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

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 206  df-an 396  df-or 844

This theorem is referenced by:  anor  979  3ianor  1105  nanor  1487  noranOLD  1529  cadnot  1618  19.33b  1889  neorian  3038  indifdirOLD  4216  2nreu  4372  tpprceq3  4734  tppreqb  4735  prneimg  4782  prnebg  4783  preq12nebg  4790  opthprneg  4792  opthneg  5390  fr2nr  5558  iresn0n0  5952  xpeq0  6052  difxp  6056  ordtri3or  6283  imadif  6502  ftpg  7010  nf1const  7156  nf1oconst  7157  0mpo0  7336  2mpo0  7496  bropopvvv  7901  bropfvvvv  7903  frxp  7938  soxp  7941  ressuppssdif  7972  mpoxneldm  7999  dfsup2  9133  nelaneq  9288  suc11reg  9307  rankxplim3  9570  kmlem3  9839  cdainflem  9874  isfin5-2  10078  mulge0b  11775  nn0n0n1ge2b  12231  rpneg  12691  mul2lt0bi  12765  xrrebnd  12831  xnn0xaddcl  12898  xmullem2  12928  difreicc  13145  fz0  13200  nelfzo  13321  injresinj  13436  hashunx  14029  swrdnd  14295  swrdnnn0nd  14297  swrdnd0  14298  repswswrd  14425  dfgcd2  16182  ncoprmlnprm  16360  firest  17060  xpcbas  17811  smndex2dnrinv  18469  symgfix2  18939  gsumdixp  19763  0ringnnzr  20453  mplsubrglem  21120  symgmatr01lem  21710  ppttop  22065  fin1aufil  22991  zclmncvs  24217  mbfmax  24718  mdegleb  25134  coemulhi  25320  numedglnl  27417  usgredg2v  27497  clwwlkn  28291  clwwlkneq0  28294  clwwlknon1nloop  28364  trlsegvdeg  28492  1to2vfriswmgr  28544  numclwwlk3lem2  28649  atcvati  30649  difrab2  30746  ofpreima2  30905  hashxpe  31029  ordtconnlem1  31776  aean  32112  sitgaddlemb  32215  ballotlemodife  32364  bnj1174  32883  erdszelem10  33062  satfv1  33225  fmla0disjsuc  33260  fmlasucdisj  33261  dfon2lem4  33668  naddcllem  33758  noetasuplem4  33866  noetainflem4  33870  sltlpss  34014  nrmo  34526  poimirlem30  35734  poimirlem31  35735  itg2addnclem  35755  itg2addnclem2  35756  itg2addnclem3  35757  iblabsnclem  35767  ftc1anclem3  35779  areacirclem4  35795  lsatcvat  36991  lkreqN  37111  cvrat  37363  4atlem3  37537  paddasslem17  37777  llnexchb2  37810  dalawlem14  37825  cdleme0nex  38231  lclkrlem2o  39462  lcfrlem19  39502  dvrelog2b  40002  aks4d1p7  40019  sticksstones1  40030  ifpnot23  40983  ifpim123g  41005  sqrtcvallem1  41128  ntrneineine1lem  41583  mnringmulrcld  41735  stoweidlem14  43445  stoweidlem26  43457  dfatprc  44509  afvco2  44555  ndmafv2nrn  44601  nfunsnafv2  44604  afv2ndeffv0  44639  nltle2tri  44693  ichnreuop  44812  spr0nelg  44816  evennodd  44983  oddneven  44984  lindslinindsimp1  45686  lindslinindsimp2  45692  line2ylem  45985  line2xlem  45987