Theorem ioran 986

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

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

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 849

This theorem is referenced by:  pm4.56  991  xor  1017  3ioran  1106  3ori  1427  ecase23d  1476  19.43OLD  1885  dfun2  4210  prneimg2  4798  prnebg  4799  sotrieq2  5571  somo  5578  dflim3  7798  frxp  8076  poxp  8078  soxp  8079  frxp2  8094  frxp3  8101  suppofssd  8153  oalimcl  8495  omlimcl  8513  oeeulem  8537  fsetexb  8811  domunfican  9232  infsupprpr  9419  ordtypelem7  9439  cantnfp1lem2  9600  cantnfp1lem3  9601  cantnflem1  9610  cnfcom2lem  9622  ssfin4  10232  fin1a2lem7  10328  fin1a2lem12  10333  fpwwe2lem12  10565  fpwwe2  10566  r1wunlim  10660  recgt0  12001  elnnz  12534  xrltlen  13097  xaddf  13176  xmullem  13216  xmullem2  13217  ssfzoulel  13715  elfznelfzo  13728  elfznelfzob  13729  om2uzf1oi  13915  fsuppmapnn0fiubex  13954  bcval4  14269  sadcaddlem  16426  lcmcllem  16565  lcmgcdlem  16575  lcmftp  16605  lcmfunsnlem2lem1  16607  lcmfunsnlem2lem2  16608  lcmfunsnlem2  16609  isprm3  16652  prmdvdsbc  16696  prm23ge5  16786  pcpremul  16814  mndpsuppss  18733  subgmulg  19116  isnirred  20400  isdomn2OLD  20689  cnfldfun  21366  mdetunilem7  22583  mndifsplit  22601  ordtbaslem  23153  iunconn  23393  fbun  23805  fin1aufil  23897  reconnlem2  24793  rrxmvallem  25371  pmltpc  25417  itg2splitlem  25715  mdegmullem  26043  atans2  26895  leibpilem2  26905  leibpi  26906  wilthlem2  27032  lgsdir2  27293  2lgslem3  27367  nosepdmlem  27647  ltsrec  27793  om2noseqf1o  28293  elnnzs  28393  ragncol  28777  opptgdim2  28813  hlpasch  28824  trgcopy  28872  cgrg3col4  28921  structiedg0val  29091  usgredg2v  29296  nb3grprlem2  29450  vtxd0nedgb  29557  1egrvtxdg0  29580  wwlksnndef  29973  nfrgr2v  30342  nonbooli  31722  cvnbtwn4  32360  chirredi  32465  atcvat4i  32468  nelun  32583  hashxpe  32880  domnmuln0rd  33335  lindssn  33438  ssdifidlprm  33518  mxidlirred  33532  bnj1304  34961  bnj1417  35183  erdszelem9  35381  satf0n0  35560  fmlaomn0  35572  fmla0disjsuc  35580  fmlasucdisj  35581  3orit  35898  dfon3  36072  dfrdg4  36133  weiunpo  36647  wl-df3maxtru1  37808  poimirlem18  37959  poimirlem21  37962  orsild  38409  orsird  38410  notornotel1  38416  cvrat4  39889  hdmaplem4  42220  mapdh9a  42235  aks6d1c5lem1  42575  redvmptabs  42792  mulltgt0d  42927  mullt0b2d  42929  sn-mullt0d  42930  dffltz  43067  fnwe2lem2  43479  dflim6  43692  ifpnot23  43905  ifpim123g  43927  ontric3g  43949  df3or2  44195  3ornot23VD  45273  ndisj2  45482  xrssre  45778  icccncfext  46315  fourierdlem42  46577  fourierdlem92  46626  salexct2  46767  nnfoctbdjlem  46883  euoreqb  47557  afvfv0bi  47600  afv2fv0  47713  ltnltne  47747  prproropf1olem4  47966  lighneallem4  48073  oddprmALTV  48163  usgrexmpl2trifr  48513  2itscp  49257  fucofvalne  49800