Theorem ioran 984

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 405	. 2 ⊢ (¬ (¬ 𝜑 → 𝜓) ↔ (¬ 𝜑 ∧ ¬ 𝜓))
2		pm4.64 848	. 2 ⊢ ((¬ 𝜑 → 𝜓) ↔ (𝜑 ∨ 𝜓))
3	1, 2	xchnxbi 332	1 ⊢ (¬ (𝜑 ∨ 𝜓) ↔ (¬ 𝜑 ∧ ¬ 𝜓))

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

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 847

This theorem is referenced by:  pm4.56  989  xor  1015  3ioran  1106  3ori  1424  ecase23d  1473  19.43OLD  1882  2ralorOLD  3238  dfun2  4289  prnebg  4880  sotrieq2  5639  somo  5646  dflim3  7884  frxp  8167  poxp  8169  soxp  8170  frxp2  8185  frxp3  8192  suppofssd  8244  oalimcl  8616  omlimcl  8634  oeeulem  8657  fsetexb  8922  domunfican  9389  infsupprpr  9573  ordtypelem7  9593  cantnfp1lem2  9748  cantnfp1lem3  9749  cantnflem1  9758  cnfcom2lem  9770  ssfin4  10379  fin1a2lem7  10475  fin1a2lem12  10480  fpwwe2lem12  10711  fpwwe2  10712  r1wunlim  10806  1re  11290  recgt0  12140  elnnz  12649  xrltlen  13208  xaddf  13286  xmullem  13326  xmullem2  13327  ssfzoulel  13810  elfznelfzo  13822  elfznelfzob  13823  om2uzf1oi  14004  fsuppmapnn0fiubex  14043  bcval4  14356  sadcaddlem  16503  lcmcllem  16643  lcmgcdlem  16653  lcmftp  16683  lcmfunsnlem2lem1  16685  lcmfunsnlem2lem2  16686  lcmfunsnlem2  16687  isprm3  16730  prmdvdsbc  16773  prm23ge5  16862  pcpremul  16890  subgmulg  19180  isnirred  20446  isdomn2OLD  20734  cnfldfun  21401  cnfldfunOLD  21414  mdetunilem7  22645  mndifsplit  22663  ordtbaslem  23217  iunconn  23457  fbun  23869  fin1aufil  23961  reconnlem2  24868  rrxmvallem  25457  pmltpc  25504  itg2splitlem  25803  mdegmullem  26137  atans2  26992  leibpilem2  27002  leibpi  27003  wilthlem2  27130  lgsdir2  27392  2lgslem3  27466  nosepdmlem  27746  sltrec  27883  om2noseqf1o  28325  elnnzs  28405  ragncol  28735  opptgdim2  28771  hlpasch  28782  trgcopy  28830  cgrg3col4  28879  structiedg0val  29057  usgredg2v  29262  nb3grprlem2  29416  vtxd0nedgb  29524  1egrvtxdg0  29547  wwlksnndef  29938  nfrgr2v  30304  nonbooli  31683  cvnbtwn4  32321  chirredi  32426  atcvat4i  32429  nelun  32542  hashxpe  32814  domnmuln0rd  33246  lindssn  33371  ssdifidlprm  33451  mxidlirred  33465  bnj1304  34795  bnj1417  35017  erdszelem9  35167  satf0n0  35346  fmlaomn0  35358  fmla0disjsuc  35366  fmlasucdisj  35367  3orit  35678  dfon3  35856  dfrdg4  35915  weiunpo  36431  wl-df3maxtru1  37458  poimirlem18  37598  poimirlem21  37601  orsild  38048  orsird  38049  notornotel1  38055  cvrat4  39400  hdmaplem4  41731  mapdh9a  41746  aks6d1c5lem1  42093  metakunt12  42173  dffltz  42589  fnwe2lem2  43008  dflim6  43226  ifpnot23  43440  ifpim123g  43462  ontric3g  43484  df3or2  43730  3ornot23VD  44818  ndisj2  44953  xrssre  45263  icccncfext  45808  fourierdlem42  46070  fourierdlem92  46119  salexct2  46260  nnfoctbdjlem  46376  euoreqb  47024  afvfv0bi  47067  afv2fv0  47180  ltnltne  47214  prproropf1olem4  47380  lighneallem4  47484  oddprmALTV  47561  usgrexmpl2trifr  47852  mndpsuppss  48096  2itscp  48515