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

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

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 401  df-or 861

This theorem is used by:  pm4.56  1004  orsild  1019  orsird  1020  xor  1032  3ioran  1123  3ori  1451  ecase23d  1503  ecase33d  1504  19.43OLD  1913  dfun2  4223  prneimg2  4820  prnebg  4821  sotrieq2  5601  somo  5608  dflim3  7839  frxp  8118  poxp  8120  soxp  8121  frxp2  8136  frxp3  8143  suppofssd  8195  oalimcl  8541  omlimcl  8559  oeeulem  8583  fsetexb  8857  domunfican  9277  infsupprpr  9462  ordtypelem7  9482  cantnfp1lem2  9644  cantnfp1lem3  9645  cantnflem1  9654  cnfcom2lem  9666  ssfin4  10298  fin1a2lem7  10394  fin1a2lem12  10399  fpwwe2lem12  10631  fpwwe2  10632  r1wunlim  10726  recgt0  12065  elnnz  12605  xrltlen  13175  xaddf  13254  xmullem  13294  xmullem2  13295  ssfzoulel  13794  elfznelfzo  13807  elfznelfzob  13808  om2uzf1oi  13994  fsuppmapnn0fiubex  14033  bcval4  14348  sadcaddlem  16519  lcmcllem  16658  lcmgcdlem  16668  lcmftp  16698  lcmfunsnlem2lem1  16700  lcmfunsnlem2lem2  16701  lcmfunsnlem2  16702  isprm3  16745  prmdvdsbc  16789  prm23ge5  16879  pcpremul  16907  mndpsuppss  18827  subgmulg  19211  isnirred  20507  ssdifidlprm  21495  prmidlsubm  21496  cnfldfun  21545  mdetunilem7  22784  mndifsplit  22802  ordtbaslem  23354  iunconn  23594  fbun  24006  fin1aufil  24098  reconnlem2  24994  rrxmvallem  25572  pmltpc  25618  itg2splitlem  25916  mdegmullem  26244  atans2  27105  leibpilem2  27115  leibpi  27116  wilthlem2  27242  lgsdir2  27503  2lgslem3  27577  nosepdmlem  27856  ltsrec  28003  om2noseqf1o  28503  elnnzs  28603  ragncol  28998  opptgdim2  29035  hlpasch  29047  trgcopy  29124  cgrg3col4  29179  prlngex  29210  prlngmid2  29220  tgaltai  29226  structiedg0val  29381  usgredg2v  29586  nb3grprlem2  29740  vtxd0nedgb  29847  1egrvtxdg0  29870  wwlksnndef  30263  nfrgr2v  30632  nonbooli  32012  cvnbtwn4  32650  chirredi  32755  atcvat4i  32758  nelun  32868  hashxpe  33161  domnmuln0rd  33606  lindssn  33700  mxidlirred  33764  dflringlem2  33794  morleylemrneab  35067  bnj1304  35216  bnj1417  35438  erdszelem9  35699  satf0n0  35878  fmlaomn0  35890  fmla0disjsuc  35898  fmlasucdisj  35899  3orit  36216  dfon3  36390  dfrdg4  36451  weiunpo  37004  wl-df3maxtru1  38166  poimirlem18  38317  poimirlem21  38320  notornotel1  38772  cvrat4  40245  hdmaplem4  42576  mapdh9a  42591  aks6d1c5lem1  42931  redvmptabs  43149  mulltgt0d  43284  mullt0b2d  43286  sn-mullt0d  43287  dffltz  43394  fnwe2lem2  43806  dflim6  44019  ifpnot23  44232  ifpim123g  44254  ontric3g  44276  df3or2  44522  3ornot23VD  45583  ndisj2  45799  xrssre  46092  icccncfext  46629  fourierdlem42  46891  fourierdlem92  46940  salexct2  47081  nnfoctbdjlem  47197  euoreqb  47874  afvfv0bi  47917  afv2fv0  48030  ltnltne  48064  prproropf1olem4  48283  lighneallem4  48390  oddprmALTV  48480  usgrexmpl2trifr  48830  2itscp  49589  fucofvalne  50131