Theorem ioran 999

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 411	. 2 ⊢ (¬ (¬ 𝜑 → 𝜓) ↔ (¬ 𝜑 ∧ ¬ 𝜓))
2		pm4.64 863	. 2 ⊢ ((¬ 𝜑 → 𝜓) ↔ (𝜑 ∨ 𝜓))
3	1, 2	xchnxbi 335	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:  pm4.56  1004  orsild  1019  orsird  1020  xor  1032  3ioran  1123  3ori  1451  ecase23d  1503  ecase33d  1504  19.43OLD  1916  dfun2  4216  prneimg2  4815  prnebg  4816  sotrieq2  5591  somo  5598  dflim3  7856  frxp  8136  poxp  8138  soxp  8139  frxp2  8154  frxp3  8161  suppofssd  8213  oalimcl  8561  omlimcl  8579  oeeulem  8603  fsetexb  8879  domunfican  9306  infsupprpr  9491  ordtypelem7  9511  cantnfp1lem2  9673  cantnfp1lem3  9674  cantnflem1  9683  cnfcom2lem  9695  ssfin4  10381  fin1a2lem7  10477  fin1a2lem12  10482  fpwwe2lem12  10720  fpwwe2  10721  r1wunlim  10815  recgt0  12156  elnnz  12696  xrltlen  13268  xaddf  13347  xmullem  13387  xmullem2  13388  ssfzoulel  13888  elfznelfzo  13901  elfznelfzob  13902  om2uzf1oi  14089  fsuppmapnn0fiubex  14128  bcval4  14444  sadcaddlem  16620  lcmcllem  16764  lcmgcdlem  16774  lcmftp  16804  lcmfunsnlem2lem1  16806  lcmfunsnlem2lem2  16807  lcmfunsnlem2  16808  isprm3  16851  prmdvdsbc  16895  prm23ge5  16986  pcpremul  17014  mndpsuppss  18952  subgmulg  19344  isnirred  20643  ssdifidlprm  21635  prmidlsubm  21636  cnfldfun  21685  mdetunilem7  22926  mndifsplit  22944  ordtbaslem  23499  iunconn  23739  fbun  24152  fin1aufil  24244  reconnlem2  25140  rrxmvallem  25718  pmltpc  25764  itg2splitlem  26062  mdegmullem  26389  atans2  27252  leibpilem2  27262  leibpi  27263  wilthlem2  27389  lgsdir2  27650  2lgslem3  27724  nosepdmlem  28033  ltsrec  28180  om2noseqf1o  28680  elnnzs  28780  ragncol  29177  opptgdim2  29214  hlpasch  29227  trgcopy  29304  tgaaddcpbllem1  29342  tgaaddcpbl  29345  cgrg3col4  29365  angmgmaddeu1  29372  angmgmaddcpbl  29383  prlngex  29422  prlngmid2  29432  tgaltai  29438  structiedg0val  29593  usgredg2v  29801  nb3grprlem2  29955  vtxd0nedgb  30062  1egrvtxdg0  30085  wwlksnndef  30487  nfrgr2v  30866  nonbooli  32246  cvnbtwn4  32884  chirredi  32989  atcvat4i  32992  nelun  33102  hashxpe  33392  domnmuln0rd  33831  lindssn  33926  mxidlirred  33990  dflringlem2  34020  morleylemrneab  35293  bnj1304  35442  bnj1417  35664  erdszelem9  35943  satf0n0  36122  fmlaomn0  36134  fmla0disjsuc  36142  fmlasucdisj  36143  3orit  36460  dfon3  36634  dfrdg4  36695  weiunpo  37233  wl-df3maxtru1  38395  poimirlem18  38536  poimirlem21  38539  notornotel1  39007  cvrat4  40480  hdmaplem4  42811  mapdh9a  42826  aks6d1c5lem1  43166  redvmptabs  43391  mulltgt0d  43526  mullt0b2d  43528  sn-mullt0d  43529  dffltz  43650  fnwe2lem2  44037  dflim6  44250  ifpnot23  44463  ifpim123g  44485  ontric3g  44507  df3or2  44753  3ornot23VD  45814  ndisj2  46037  xrssre  46329  icccncfext  46866  fourierdlem42  47128  fourierdlem92  47177  salexct2  47318  nnfoctbdjlem  47434  euoreqb  48148  afvfv0bi  48191  afv2fv0  48304  ltnltne  48338  prproropf1olem4  48557  lighneallem4  48664  oddprmALTV  48754  usgrexmpl2trifr  49104  2itscp  49862  fucofvalne  50402