Theorem ioran 996

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

Syntax hints:  ¬ wn 3   → wi 4   ↔ wb 208   ∧ wa 399   ∨ wo 858

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 209  df-an 400  df-or 859

This theorem is referenced by:  pm4.56  1001  xor  1027  3ioran  1117  3ori  1442  ecase23d  1493  19.43OLD  1902  dfun2  4220  prneimg2  4810  prnebg  4811  sotrieq2  5583  somo  5590  dflim3  7822  frxp  8100  poxp  8102  soxp  8103  frxp2  8118  frxp3  8125  suppofssd  8177  oalimcl  8523  omlimcl  8541  oeeulem  8565  fsetexb  8839  domunfican  9260  infsupprpr  9446  ordtypelem7  9466  cantnfp1lem2  9628  cantnfp1lem3  9629  cantnflem1  9638  cnfcom2lem  9650  ssfin4  10261  fin1a2lem7  10357  fin1a2lem12  10362  fpwwe2lem12  10594  fpwwe2  10595  r1wunlim  10689  recgt0  12031  elnnz  12572  xrltlen  13142  xaddf  13221  xmullem  13261  xmullem2  13262  ssfzoulel  13760  elfznelfzo  13773  elfznelfzob  13774  om2uzf1oi  13960  fsuppmapnn0fiubex  13999  bcval4  14314  sadcaddlem  16482  lcmcllem  16621  lcmgcdlem  16631  lcmftp  16661  lcmfunsnlem2lem1  16663  lcmfunsnlem2lem2  16664  lcmfunsnlem2  16665  isprm3  16708  prmdvdsbc  16752  prm23ge5  16842  pcpremul  16870  mndpsuppss  18790  subgmulg  19173  isnirred  20456  isdomn2OLD  20749  cnfldfun  21426  mdetunilem7  22666  mndifsplit  22684  ordtbaslem  23236  iunconn  23476  fbun  23888  fin1aufil  23980  reconnlem2  24876  rrxmvallem  25454  pmltpc  25500  itg2splitlem  25798  mdegmullem  26126  atans2  26984  leibpilem2  26994  leibpi  26995  wilthlem2  27121  lgsdir2  27382  2lgslem3  27456  nosepdmlem  27735  ltsrec  27882  om2noseqf1o  28382  elnnzs  28482  ragncol  28866  opptgdim2  28902  hlpasch  28913  trgcopy  28961  cgrg3col4  29010  structiedg0val  29180  usgredg2v  29385  nb3grprlem2  29539  vtxd0nedgb  29646  1egrvtxdg0  29669  wwlksnndef  30062  nfrgr2v  30431  nonbooli  31811  cvnbtwn4  32449  chirredi  32554  atcvat4i  32557  nelun  32672  hashxpe  32970  domnmuln0rd  33419  lindssn  33525  ssdifidlprm  33606  prmidlsubm  33607  mxidlirred  33621  dflringlem2  33652  morleylemrneab  34926  bnj1304  35075  bnj1417  35297  erdszelem9  35510  satf0n0  35689  fmlaomn0  35701  fmla0disjsuc  35709  fmlasucdisj  35710  3orit  36027  dfon3  36201  dfrdg4  36262  weiunpo  36786  wl-df3maxtru1  37947  poimirlem18  38098  poimirlem21  38101  orsild  38548  orsird  38549  notornotel1  38555  cvrat4  40028  hdmaplem4  42359  mapdh9a  42374  aks6d1c5lem1  42714  redvmptabs  42930  mulltgt0d  43065  mullt0b2d  43067  sn-mullt0d  43068  dffltz  43177  fnwe2lem2  43589  dflim6  43802  ifpnot23  44015  ifpim123g  44037  ontric3g  44059  df3or2  44305  3ornot23VD  45383  ndisj2  45592  xrssre  45885  icccncfext  46422  fourierdlem42  46684  fourierdlem92  46733  salexct2  46874  nnfoctbdjlem  46990  euoreqb  47664  afvfv0bi  47707  afv2fv0  47820  ltnltne  47854  prproropf1olem4  48073  lighneallem4  48180  oddprmALTV  48270  usgrexmpl2trifr  48620  2itscp  49364  fucofvalne  49907