Theorem ioran 980

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

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

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 206  df-an 396  df-or 844

This theorem is referenced by:  pm4.56  985  xor  1011  3ioran  1104  3ori  1422  ecase23d  1471  noranOLD  1529  norassOLD  1536  19.43OLD  1887  2ralorOLD  3295  dfun2  4190  prnebg  4783  sotrieq2  5524  somo  5531  dflim3  7669  frxp  7938  poxp  7940  soxp  7941  suppofssd  7990  oalimcl  8353  omlimcl  8371  oeeulem  8394  fsetexb  8610  domunfican  9017  infsupprpr  9193  ordtypelem7  9213  cantnfp1lem2  9367  cantnfp1lem3  9368  cantnflem1  9377  cnfcom2lem  9389  ssfin4  9997  fin1a2lem7  10093  fin1a2lem12  10098  fpwwe2lem12  10329  fpwwe2  10330  r1wunlim  10424  1re  10906  recgt0  11751  elnnz  12259  xrltlen  12809  xaddf  12887  xmullem  12927  xmullem2  12928  ssfzoulel  13409  elfznelfzo  13420  elfznelfzob  13421  om2uzf1oi  13601  fsuppmapnn0fiubex  13640  bcval4  13949  sadcaddlem  16092  lcmcllem  16229  lcmgcdlem  16239  lcmftp  16269  lcmfunsnlem2lem1  16271  lcmfunsnlem2lem2  16272  lcmfunsnlem2  16273  isprm3  16316  prm23ge5  16444  pcpremul  16472  subgmulg  18684  isnirred  19857  isdomn2  20483  cnfldfunALT  20523  mdetunilem7  21675  mndifsplit  21693  ordtbaslem  22247  iunconn  22487  fbun  22899  fin1aufil  22991  reconnlem2  23896  rrxmvallem  24473  pmltpc  24519  itg2splitlem  24818  mdegmullem  25148  atans2  25986  leibpilem2  25996  leibpi  25997  wilthlem2  26123  lgsdir2  26383  2lgslem3  26457  ragncol  26974  opptgdim2  27010  hlpasch  27021  trgcopy  27069  cgrg3col4  27118  structiedg0val  27295  usgredg2v  27497  nb3grprlem2  27651  vtxd0nedgb  27758  1egrvtxdg0  27781  wwlksnndef  28171  nfrgr2v  28537  nonbooli  29914  cvnbtwn4  30552  chirredi  30657  atcvat4i  30660  nelun  30760  hashxpe  31029  prmdvdsbc  31032  lindssn  31475  bnj1304  32699  bnj1417  32921  erdszelem9  33061  satf0n0  33240  fmlaomn0  33252  fmla0disjsuc  33260  fmlasucdisj  33261  3orit  33560  frxp2  33718  frxp3  33724  nosepdmlem  33813  sltrec  33941  dfon3  34121  dfrdg4  34180  wl-df3maxtru1  35590  poimirlem18  35722  poimirlem21  35725  orsild  36173  orsird  36174  notornotel1  36180  cvrat4  37384  hdmaplem4  39715  mapdh9a  39730  metakunt12  40064  dffltz  40387  fnwe2lem2  40792  ifpnot23  40983  ifpim123g  41005  ontric3g  41027  df3or2  41265  3ornot23VD  42356  ndisj2  42488  xrssre  42777  icccncfext  43318  fourierdlem42  43580  fourierdlem92  43629  salexct2  43768  nnfoctbdjlem  43883  euoreqb  44488  afvfv0bi  44531  afv2fv0  44644  ltnltne  44679  prproropf1olem4  44846  lighneallem4  44950  oddprmALTV  45027  mndpsuppss  45595  2itscp  46015