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  1423  ecase23d  1472  19.43OLD  1880  2ralorOLD  3229  dfun2  4275  prneimg2  4859  prnebg  4860  sotrieq2  5627  somo  5634  dflim3  7867  frxp  8149  poxp  8151  soxp  8152  frxp2  8167  frxp3  8174  suppofssd  8226  oalimcl  8596  omlimcl  8614  oeeulem  8637  fsetexb  8902  domunfican  9358  infsupprpr  9541  ordtypelem7  9561  cantnfp1lem2  9716  cantnfp1lem3  9717  cantnflem1  9726  cnfcom2lem  9738  ssfin4  10347  fin1a2lem7  10443  fin1a2lem12  10448  fpwwe2lem12  10679  fpwwe2  10680  r1wunlim  10774  1re  11258  recgt0  12110  elnnz  12620  xrltlen  13184  xaddf  13262  xmullem  13302  xmullem2  13303  ssfzoulel  13795  elfznelfzo  13807  elfznelfzob  13808  om2uzf1oi  13990  fsuppmapnn0fiubex  14029  bcval4  14342  sadcaddlem  16490  lcmcllem  16629  lcmgcdlem  16639  lcmftp  16669  lcmfunsnlem2lem1  16671  lcmfunsnlem2lem2  16672  lcmfunsnlem2  16673  isprm3  16716  prmdvdsbc  16759  prm23ge5  16848  pcpremul  16876  mndpsuppss  18790  subgmulg  19170  isnirred  20436  isdomn2OLD  20728  cnfldfun  21395  cnfldfunOLD  21408  mdetunilem7  22639  mndifsplit  22657  ordtbaslem  23211  iunconn  23451  fbun  23863  fin1aufil  23955  reconnlem2  24862  rrxmvallem  25451  pmltpc  25498  itg2splitlem  25797  mdegmullem  26131  atans2  26988  leibpilem2  26998  leibpi  26999  wilthlem2  27126  lgsdir2  27388  2lgslem3  27462  nosepdmlem  27742  sltrec  27879  om2noseqf1o  28321  elnnzs  28401  ragncol  28731  opptgdim2  28767  hlpasch  28778  trgcopy  28826  cgrg3col4  28875  structiedg0val  29053  usgredg2v  29258  nb3grprlem2  29412  vtxd0nedgb  29520  1egrvtxdg0  29543  wwlksnndef  29934  nfrgr2v  30300  nonbooli  31679  cvnbtwn4  32317  chirredi  32422  atcvat4i  32425  nelun  32540  hashxpe  32816  domnmuln0rd  33260  lindssn  33385  ssdifidlprm  33465  mxidlirred  33479  bnj1304  34811  bnj1417  35033  erdszelem9  35183  satf0n0  35362  fmlaomn0  35374  fmla0disjsuc  35382  fmlasucdisj  35383  3orit  35695  dfon3  35873  dfrdg4  35932  weiunpo  36447  wl-df3maxtru1  37474  poimirlem18  37624  poimirlem21  37627  orsild  38074  orsird  38075  notornotel1  38081  cvrat4  39425  hdmaplem4  41756  mapdh9a  41771  aks6d1c5lem1  42117  metakunt12  42197  redvmptabs  42368  dffltz  42620  fnwe2lem2  43039  dflim6  43253  ifpnot23  43467  ifpim123g  43489  ontric3g  43511  df3or2  43757  3ornot23VD  44844  ndisj2  44990  xrssre  45297  icccncfext  45842  fourierdlem42  46104  fourierdlem92  46153  salexct2  46294  nnfoctbdjlem  46410  euoreqb  47058  afvfv0bi  47101  afv2fv0  47214  ltnltne  47248  prproropf1olem4  47430  lighneallem4  47534  oddprmALTV  47611  usgrexmpl2trifr  47931  2itscp  48630