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 ⊢ (¬ (𝜑 ∨ 𝜓) ↔ (¬ 𝜑 ∧ ¬ 𝜓))

Syntax hints:  ¬ wn 3   → wi 4   ↔ wb 209   ∧ wa 400   ∨ wo 860

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

This theorem is referenced by:  pm4.56  1004  xor  1030  3ioran  1121  3ori  1449  ecase23d  1500  ecase33d  1501  19.43OLD  1910  dfun2  4231  prneimg2  4821  prnebg  4822  sotrieq2  5599  somo  5606  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  10290  fin1a2lem7  10386  fin1a2lem12  10391  fpwwe2lem12  10623  fpwwe2  10624  r1wunlim  10718  recgt0  12057  elnnz  12597  xrltlen  13167  xaddf  13246  xmullem  13286  xmullem2  13287  ssfzoulel  13785  elfznelfzo  13798  elfznelfzob  13799  om2uzf1oi  13985  fsuppmapnn0fiubex  14024  bcval4  14339  sadcaddlem  16511  lcmcllem  16650  lcmgcdlem  16660  lcmftp  16690  lcmfunsnlem2lem1  16692  lcmfunsnlem2lem2  16693  lcmfunsnlem2  16694  isprm3  16737  prmdvdsbc  16781  prm23ge5  16871  pcpremul  16899  mndpsuppss  18819  subgmulg  19203  isnirred  20498  ssdifidlprm  21451  prmidlsubm  21452  cnfldfun  21501  mdetunilem7  22740  mndifsplit  22758  ordtbaslem  23310  iunconn  23550  fbun  23962  fin1aufil  24054  reconnlem2  24950  rrxmvallem  25528  pmltpc  25574  itg2splitlem  25872  mdegmullem  26200  atans2  27058  leibpilem2  27068  leibpi  27069  wilthlem2  27195  lgsdir2  27456  2lgslem3  27530  nosepdmlem  27809  ltsrec  27956  om2noseqf1o  28456  elnnzs  28556  ragncol  28944  opptgdim2  28981  hlpasch  28993  trgcopy  29068  cgrg3col4  29121  prlngex  29150  structiedg0val  29309  usgredg2v  29514  nb3grprlem2  29668  vtxd0nedgb  29775  1egrvtxdg0  29798  wwlksnndef  30191  nfrgr2v  30560  nonbooli  31940  cvnbtwn4  32578  chirredi  32683  atcvat4i  32686  nelun  32796  hashxpe  33089  domnmuln0rd  33534  lindssn  33631  mxidlirred  33696  dflringlem2  33726  morleylemrneab  34999  bnj1304  35148  bnj1417  35370  erdszelem9  35586  satf0n0  35765  fmlaomn0  35777  fmla0disjsuc  35785  fmlasucdisj  35786  3orit  36103  dfon3  36277  dfrdg4  36338  weiunpo  36861  wl-df3maxtru1  38021  poimirlem18  38172  poimirlem21  38175  orsild  38622  orsird  38623  notornotel1  38629  cvrat4  40102  hdmaplem4  42433  mapdh9a  42448  aks6d1c5lem1  42788  redvmptabs  43006  mulltgt0d  43141  mullt0b2d  43143  sn-mullt0d  43144  dffltz  43253  fnwe2lem2  43665  dflim6  43878  ifpnot23  44091  ifpim123g  44113  ontric3g  44135  df3or2  44381  3ornot23VD  45442  ndisj2  45658  xrssre  45951  icccncfext  46488  fourierdlem42  46750  fourierdlem92  46799  salexct2  46940  nnfoctbdjlem  47056  euoreqb  47730  afvfv0bi  47773  afv2fv0  47886  ltnltne  47920  prproropf1olem4  48139  lighneallem4  48246  oddprmALTV  48336  usgrexmpl2trifr  48686  2itscp  49441  fucofvalne  49983