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  4223  prneimg2  4822  prnebg  4823  sotrieq2  5603  somo  5610  dflim3  7845  frxp  8124  poxp  8126  soxp  8127  frxp2  8142  frxp3  8149  suppofssd  8201  oalimcl  8547  omlimcl  8565  oeeulem  8589  fsetexb  8863  domunfican  9284  infsupprpr  9469  ordtypelem7  9489  cantnfp1lem2  9651  cantnfp1lem3  9652  cantnflem1  9661  cnfcom2lem  9673  ssfin4  10305  fin1a2lem7  10401  fin1a2lem12  10406  fpwwe2lem12  10638  fpwwe2  10639  r1wunlim  10733  recgt0  12072  elnnz  12612  xrltlen  13183  xaddf  13262  xmullem  13302  xmullem2  13303  ssfzoulel  13802  elfznelfzo  13815  elfznelfzob  13816  om2uzf1oi  14003  fsuppmapnn0fiubex  14042  bcval4  14357  sadcaddlem  16533  lcmcllem  16672  lcmgcdlem  16682  lcmftp  16712  lcmfunsnlem2lem1  16714  lcmfunsnlem2lem2  16715  lcmfunsnlem2  16716  isprm3  16759  prmdvdsbc  16803  prm23ge5  16893  pcpremul  16921  mndpsuppss  18847  subgmulg  19231  isnirred  20528  ssdifidlprm  21516  prmidlsubm  21517  cnfldfun  21566  mdetunilem7  22805  mndifsplit  22823  ordtbaslem  23375  iunconn  23615  fbun  24028  fin1aufil  24120  reconnlem2  25016  rrxmvallem  25594  pmltpc  25640  itg2splitlem  25938  mdegmullem  26266  atans2  27127  leibpilem2  27137  leibpi  27138  wilthlem2  27264  lgsdir2  27525  2lgslem3  27599  nosepdmlem  27878  ltsrec  28025  om2noseqf1o  28525  elnnzs  28625  ragncol  29020  opptgdim2  29057  hlpasch  29069  trgcopy  29146  cgrg3col4  29201  prlngex  29232  prlngmid2  29242  tgaltai  29248  structiedg0val  29403  usgredg2v  29611  nb3grprlem2  29765  vtxd0nedgb  29872  1egrvtxdg0  29895  wwlksnndef  30297  nfrgr2v  30670  nonbooli  32050  cvnbtwn4  32688  chirredi  32793  atcvat4i  32796  nelun  32906  hashxpe  33198  domnmuln0rd  33637  lindssn  33731  mxidlirred  33795  dflringlem2  33825  morleylemrneab  35099  bnj1304  35248  bnj1417  35470  erdszelem9  35704  satf0n0  35883  fmlaomn0  35895  fmla0disjsuc  35903  fmlasucdisj  35904  3orit  36221  dfon3  36395  dfrdg4  36456  weiunpo  37009  wl-df3maxtru1  38171  poimirlem18  38322  poimirlem21  38325  notornotel1  38777  cvrat4  40250  hdmaplem4  42581  mapdh9a  42596  aks6d1c5lem1  42936  redvmptabs  43154  mulltgt0d  43289  mullt0b2d  43291  sn-mullt0d  43292  dffltz  43399  fnwe2lem2  43811  dflim6  44024  ifpnot23  44237  ifpim123g  44259  ontric3g  44281  df3or2  44527  3ornot23VD  45588  ndisj2  45804  xrssre  46097  icccncfext  46634  fourierdlem42  46896  fourierdlem92  46945  salexct2  47086  nnfoctbdjlem  47202  euoreqb  47879  afvfv0bi  47922  afv2fv0  48035  ltnltne  48069  prproropf1olem4  48288  lighneallem4  48395  oddprmALTV  48485  usgrexmpl2trifr  48835  2itscp  49594  fucofvalne  50136