Theorem ioran 981

Description: Negated disjunction in terms of conjunction (De Morgan's law). Compare Theorem *4.56 of [WhiteheadRussell] p. 120. (Contributed by NM, 3-Jan-1993.) (Proof shortened by Andrew Salmon, 7-May-2011.)

Assertion

Ref	Expression
ioran	⊢ (¬ (𝜑 ∨ 𝜓) ↔ (¬ 𝜑 ∧ ¬ 𝜓))

Proof of Theorem ioran

Step	Hyp	Ref	Expression
1		pm4.65 404	. 2 ⊢ (¬ (¬ 𝜑 → 𝜓) ↔ (¬ 𝜑 ∧ ¬ 𝜓))
2		pm4.64 847	. 2 ⊢ ((¬ 𝜑 → 𝜓) ↔ (𝜑 ∨ 𝜓))
3	1, 2	xchnxbi 331	1 ⊢ (¬ (𝜑 ∨ 𝜓) ↔ (¬ 𝜑 ∧ ¬ 𝜓))

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

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 395  df-or 846

This theorem is referenced by:  pm4.56  986  xor  1012  3ioran  1103  3ori  1421  ecase23d  1470  19.43OLD  1879  2ralorOLD  3220  dfun2  4261  prnebg  4862  sotrieq2  5624  somo  5631  dflim3  7857  frxp  8140  poxp  8142  soxp  8143  frxp2  8158  frxp3  8165  suppofssd  8218  oalimcl  8590  omlimcl  8608  oeeulem  8631  fsetexb  8893  domunfican  9363  infsupprpr  9547  ordtypelem7  9567  cantnfp1lem2  9722  cantnfp1lem3  9723  cantnflem1  9732  cnfcom2lem  9744  ssfin4  10353  fin1a2lem7  10449  fin1a2lem12  10454  fpwwe2lem12  10685  fpwwe2  10686  r1wunlim  10780  1re  11264  recgt0  12111  elnnz  12620  xrltlen  13179  xaddf  13257  xmullem  13297  xmullem2  13298  ssfzoulel  13780  elfznelfzo  13792  elfznelfzob  13793  om2uzf1oi  13973  fsuppmapnn0fiubex  14012  bcval4  14324  sadcaddlem  16457  lcmcllem  16597  lcmgcdlem  16607  lcmftp  16637  lcmfunsnlem2lem1  16639  lcmfunsnlem2lem2  16640  lcmfunsnlem2  16641  isprm3  16684  prmdvdsbc  16728  prm23ge5  16817  pcpremul  16845  subgmulg  19134  isnirred  20402  isdomn2OLD  20690  cnfldfun  21357  cnfldfunOLD  21370  mdetunilem7  22611  mndifsplit  22629  ordtbaslem  23183  iunconn  23423  fbun  23835  fin1aufil  23927  reconnlem2  24834  rrxmvallem  25423  pmltpc  25470  itg2splitlem  25769  mdegmullem  26105  atans2  26959  leibpilem2  26969  leibpi  26970  wilthlem2  27097  lgsdir2  27359  2lgslem3  27433  nosepdmlem  27713  sltrec  27850  om2noseqf1o  28275  ragncol  28636  opptgdim2  28672  hlpasch  28683  trgcopy  28731  cgrg3col4  28780  structiedg0val  28958  usgredg2v  29163  nb3grprlem2  29317  vtxd0nedgb  29425  1egrvtxdg0  29448  wwlksnndef  29839  nfrgr2v  30205  nonbooli  31584  cvnbtwn4  32222  chirredi  32327  atcvat4i  32330  nelun  32439  hashxpe  32711  domnmuln0rd  33129  lindssn  33253  ssdifidlprm  33333  mxidlirred  33347  bnj1304  34664  bnj1417  34886  erdszelem9  35027  satf0n0  35206  fmlaomn0  35218  fmla0disjsuc  35226  fmlasucdisj  35227  3orit  35538  dfon3  35716  dfrdg4  35775  wl-df3maxtru1  37199  poimirlem18  37339  poimirlem21  37342  orsild  37789  orsird  37790  notornotel1  37796  cvrat4  39142  hdmaplem4  41473  mapdh9a  41488  aks6d1c5lem1  41834  metakunt12  41902  dffltz  42288  fnwe2lem2  42712  dflim6  42930  ifpnot23  43145  ifpim123g  43167  ontric3g  43189  df3or2  43435  3ornot23VD  44523  ndisj2  44652  xrssre  44963  icccncfext  45508  fourierdlem42  45770  fourierdlem92  45819  salexct2  45960  nnfoctbdjlem  46076  euoreqb  46722  afvfv0bi  46765  afv2fv0  46878  ltnltne  46912  prproropf1olem4  47078  lighneallem4  47182  oddprmALTV  47259  mndpsuppss  47750  2itscp  48169