Theorem ioran 985

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

Syntax hints:  ¬ wn 3   → wi 4   ↔ wb 206   ∧ wa 395   ∨ wo 847

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 207  df-an 396  df-or 848

This theorem is referenced by:  pm4.56  990  xor  1016  3ioran  1105  3ori  1426  ecase23d  1475  19.43OLD  1883  2ralorOLD  3216  dfun2  4245  prneimg2  4831  prnebg  4832  sotrieq2  5593  somo  5600  dflim3  7840  frxp  8123  poxp  8125  soxp  8126  frxp2  8141  frxp3  8148  suppofssd  8200  oalimcl  8570  omlimcl  8588  oeeulem  8611  fsetexb  8876  domunfican  9331  infsupprpr  9516  ordtypelem7  9536  cantnfp1lem2  9691  cantnfp1lem3  9692  cantnflem1  9701  cnfcom2lem  9713  ssfin4  10322  fin1a2lem7  10418  fin1a2lem12  10423  fpwwe2lem12  10654  fpwwe2  10655  r1wunlim  10749  1re  11233  recgt0  12085  elnnz  12596  xrltlen  13160  xaddf  13238  xmullem  13278  xmullem2  13279  ssfzoulel  13774  elfznelfzo  13786  elfznelfzob  13787  om2uzf1oi  13969  fsuppmapnn0fiubex  14008  bcval4  14323  sadcaddlem  16474  lcmcllem  16613  lcmgcdlem  16623  lcmftp  16653  lcmfunsnlem2lem1  16655  lcmfunsnlem2lem2  16656  lcmfunsnlem2  16657  isprm3  16700  prmdvdsbc  16743  prm23ge5  16833  pcpremul  16861  mndpsuppss  18741  subgmulg  19121  isnirred  20378  isdomn2OLD  20670  cnfldfun  21327  cnfldfunOLD  21340  mdetunilem7  22554  mndifsplit  22572  ordtbaslem  23124  iunconn  23364  fbun  23776  fin1aufil  23868  reconnlem2  24765  rrxmvallem  25354  pmltpc  25401  itg2splitlem  25699  mdegmullem  26033  atans2  26891  leibpilem2  26901  leibpi  26902  wilthlem2  27029  lgsdir2  27291  2lgslem3  27365  nosepdmlem  27645  sltrec  27782  om2noseqf1o  28224  elnnzs  28304  ragncol  28634  opptgdim2  28670  hlpasch  28681  trgcopy  28729  cgrg3col4  28778  structiedg0val  28947  usgredg2v  29152  nb3grprlem2  29306  vtxd0nedgb  29414  1egrvtxdg0  29437  wwlksnndef  29833  nfrgr2v  30199  nonbooli  31578  cvnbtwn4  32216  chirredi  32321  atcvat4i  32324  nelun  32440  hashxpe  32732  domnmuln0rd  33215  lindssn  33339  ssdifidlprm  33419  mxidlirred  33433  bnj1304  34796  bnj1417  35018  erdszelem9  35167  satf0n0  35346  fmlaomn0  35358  fmla0disjsuc  35366  fmlasucdisj  35367  3orit  35679  dfon3  35856  dfrdg4  35915  weiunpo  36429  wl-df3maxtru1  37456  poimirlem18  37608  poimirlem21  37611  orsild  38058  orsird  38059  notornotel1  38065  cvrat4  39408  hdmaplem4  41739  mapdh9a  41754  aks6d1c5lem1  42095  metakunt12  42175  redvmptabs  42350  dffltz  42604  fnwe2lem2  43022  dflim6  43235  ifpnot23  43449  ifpim123g  43471  ontric3g  43493  df3or2  43739  3ornot23VD  44819  ndisj2  45023  xrssre  45323  icccncfext  45864  fourierdlem42  46126  fourierdlem92  46175  salexct2  46316  nnfoctbdjlem  46432  euoreqb  47086  afvfv0bi  47129  afv2fv0  47242  ltnltne  47276  prproropf1olem4  47468  lighneallem4  47572  oddprmALTV  47649  usgrexmpl2trifr  47989  2itscp  48709  fucofvalne  49184