Theorem ianor 997

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

This proof depends on syntax axioms:  ¬ wn 3   → wi 4   ↔ wb 209   ∧ wa 401   ∨ wo 861

This proof depends on axioms:  ax-mp 5  ax-1 6  ax-2 7  ax-3 8

This proof depends on definitions:  df-bi 210  df-an 402  df-or 862

This theorem is used by:  anor  998  3ianor  1124  nanor  1524  cadnot  1647  19.33b  1917  neorian  3050  2nreu  4401  tpprceq3  4763  tppreqb  4764  prneimg  4808  prneimg2  4809  prnebg  4810  preq12nebg  4817  opthprneg  4819  opthneg  5449  fr2nr  5627  iresn0n0  6047  xpeq0  6152  difxp  6156  ordtri3or  6397  imadif  6627  ftpg  7163  nf1const  7314  nf1oconst  7315  0mpo0  7505  2mpo0  7672  bropopvvv  8103  bropfvvvv  8105  frxp  8142  soxp  8145  ressuppssdif  8207  mpoxneldm  8234  naddcllem  8690  dfsup2  9441  nelaneqOLDOLD  9603  suc11reg  9625  rankxplim3  9903  kmlem3  10236  cdainflem  10271  isfin5-2  10474  mulge0b  12192  nn0n0n1ge2b  12680  rpneg  13159  mul2lt0bi  13233  xrrebnd  13303  xnn0xaddcl  13370  xmullem2  13400  difreicc  13620  fz0  13677  nelfzo  13804  injresinj  13931  hashunx  14535  swrdnd  14810  swrdnnn0nd  14812  swrdnd0  14813  repswswrd  14941  dfgcd2  16726  ncoprmlnprm  16911  firest  17610  xpcbas  18359  smndex2dnrinv  19121  symgfix2  19637  gsumdixp  20555  0ringnnzr  20783  isfieldidl  21547  mplsubrglem  22318  symgmatr01lem  22975  ppttop  23332  fin1aufil  24258  zclmncvs  25476  mbfmax  25977  mdegleb  26389  coemulhi  26580  noetasuplem4  28100  noetainflem4  28104  ltslpss  28301  lnssplng  29277  numedglnl  29729  usgredg2v  29815  clwwlkn  30624  clwwlkneq0  30627  clwwlknon1nloop  30697  trlsegvdeg  30835  1to2vfriswmgr  30887  numclwwlk3lem2  30992  atcvati  32995  difrab2  33143  ofpreima2  33309  hashxpe  33447  drnglring  34072  fldextrspunlsplem  34353  ordtconnlem1  34604  aean  34925  sitgaddlemb  35028  ballotlemodife  35178  bnj1174  35681  erdszelem10  36053  satfv1  36216  fmla0disjsuc  36251  fmlasucdisj  36252  mirimanoffr  36548  dfon2lem4  36642  ltnadd  37061  naddle  37062  nrmo  37292  poimirlem30  38675  poimirlem31  38676  itg2addnclem  38696  itg2addnclem2  38697  itg2addnclem3  38698  iblabsnclem  38708  ftc1anclem3  38720  areacirclem4  38736  lsatcvat  40214  lkreqN  40334  cvrat  40586  4atlem3  40760  paddasslem17  41000  llnexchb2  41033  dalawlem14  41048  cdleme0nex  41454  lclkrlem2o  42685  lcfrlem19  42725  dvrelog2b  43223  aks4d1p7  43240  aks6d1c2p2  43276  aks6d1c5  43296  sticksstones1  43303  aks6d1c6lem3  43329  ifpnot23  44586  ifpim123g  44608  sqrtcvallem1  44738  ntrneineine1lem  45191  mnringmulrcld  45333  stoweidlem14  47131  stoweidlem26  47143  dfatprc  48307  afvco2  48353  ndmafv2nrn  48399  nfunsnafv2  48402  afv2ndeffv0  48437  nltle2tri  48490  ichnreuop  48661  spr0nelg  48665  evennodd  48848  oddneven  48849  usgrexmpl2trifr  49242  pg4cyclnex  49332  lindslinindsimp1  49676  lindslinindsimp2  49682  line2ylem  49970  line2xlem  49972