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  5595  somo  5602  dflim3  7843  frxp  8124  poxp  8126  soxp  8127  frxp2  8142  frxp3  8149  suppofssd  8201  oalimcl  8547  omlimcl  8565  oeeulem  8589  fsetexb  8865  domunfican  9291  infsupprpr  9476  ordtypelem7  9496  cantnfp1lem2  9658  cantnfp1lem3  9659  cantnflem1  9668  cnfcom2lem  9680  ssfin4  10312  fin1a2lem7  10408  fin1a2lem12  10413  fpwwe2lem12  10651  fpwwe2  10652  r1wunlim  10746  recgt0  12085  elnnz  12625  xrltlen  13197  xaddf  13276  xmullem  13316  xmullem2  13317  ssfzoulel  13816  elfznelfzo  13829  elfznelfzob  13830  om2uzf1oi  14017  fsuppmapnn0fiubex  14056  bcval4  14371  sadcaddlem  16547  lcmcllem  16686  lcmgcdlem  16696  lcmftp  16726  lcmfunsnlem2lem1  16728  lcmfunsnlem2lem2  16729  lcmfunsnlem2  16730  isprm3  16773  prmdvdsbc  16817  prm23ge5  16907  pcpremul  16935  mndpsuppss  18872  subgmulg  19264  isnirred  20561  ssdifidlprm  21549  prmidlsubm  21550  cnfldfun  21599  mdetunilem7  22840  mndifsplit  22858  ordtbaslem  23413  iunconn  23653  fbun  24066  fin1aufil  24158  reconnlem2  25054  rrxmvallem  25632  pmltpc  25678  itg2splitlem  25976  mdegmullem  26303  atans2  27168  leibpilem2  27178  leibpi  27179  wilthlem2  27305  lgsdir2  27566  2lgslem3  27640  nosepdmlem  27919  ltsrec  28066  om2noseqf1o  28566  elnnzs  28666  ragncol  29063  opptgdim2  29100  hlpasch  29113  trgcopy  29190  tgaaddcpbllem1  29228  tgaaddcpbl  29231  cgrg3col4  29251  angmgmaddeu1  29258  angmgmaddcpbl  29269  prlngex  29308  prlngmid2  29318  tgaltai  29324  structiedg0val  29479  usgredg2v  29687  nb3grprlem2  29841  vtxd0nedgb  29948  1egrvtxdg0  29971  wwlksnndef  30373  nfrgr2v  30752  nonbooli  32132  cvnbtwn4  32770  chirredi  32875  atcvat4i  32878  nelun  32988  hashxpe  33278  domnmuln0rd  33717  lindssn  33811  mxidlirred  33875  dflringlem2  33905  morleylemrneab  35179  bnj1304  35328  bnj1417  35550  erdszelem9  35778  satf0n0  35957  fmlaomn0  35969  fmla0disjsuc  35977  fmlasucdisj  35978  3orit  36295  dfon3  36469  dfrdg4  36530  weiunpo  37084  wl-df3maxtru1  38246  poimirlem18  38387  poimirlem21  38390  notornotel1  38843  cvrat4  40316  hdmaplem4  42647  mapdh9a  42662  aks6d1c5lem1  43002  redvmptabs  43235  mulltgt0d  43370  mullt0b2d  43372  sn-mullt0d  43373  dffltz  43480  fnwe2lem2  43892  dflim6  44105  ifpnot23  44318  ifpim123g  44340  ontric3g  44362  df3or2  44608  3ornot23VD  45669  ndisj2  45885  xrssre  46178  icccncfext  46715  fourierdlem42  46977  fourierdlem92  47026  salexct2  47167  nnfoctbdjlem  47283  euoreqb  47997  afvfv0bi  48040  afv2fv0  48153  ltnltne  48187  prproropf1olem4  48406  lighneallem4  48513  oddprmALTV  48603  usgrexmpl2trifr  48953  2itscp  49711  fucofvalne  50251