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  1884  dfun2  4222  prneimg2  4811  prnebg  4812  sotrieq2  5564  somo  5571  dflim3  7789  frxp  8068  poxp  8070  soxp  8071  frxp2  8086  frxp3  8093  suppofssd  8145  oalimcl  8487  omlimcl  8505  oeeulem  8529  fsetexb  8801  domunfican  9222  infsupprpr  9409  ordtypelem7  9429  cantnfp1lem2  9588  cantnfp1lem3  9589  cantnflem1  9598  cnfcom2lem  9610  ssfin4  10220  fin1a2lem7  10316  fin1a2lem12  10321  fpwwe2lem12  10553  fpwwe2  10554  r1wunlim  10648  recgt0  11987  elnnz  12498  xrltlen  13060  xaddf  13139  xmullem  13179  xmullem2  13180  ssfzoulel  13676  elfznelfzo  13689  elfznelfzob  13690  om2uzf1oi  13876  fsuppmapnn0fiubex  13915  bcval4  14230  sadcaddlem  16384  lcmcllem  16523  lcmgcdlem  16533  lcmftp  16563  lcmfunsnlem2lem1  16565  lcmfunsnlem2lem2  16566  lcmfunsnlem2  16567  isprm3  16610  prmdvdsbc  16653  prm23ge5  16743  pcpremul  16771  mndpsuppss  18690  subgmulg  19070  isnirred  20356  isdomn2OLD  20645  cnfldfun  21323  cnfldfunOLD  21336  mdetunilem7  22562  mndifsplit  22580  ordtbaslem  23132  iunconn  23372  fbun  23784  fin1aufil  23876  reconnlem2  24772  rrxmvallem  25360  pmltpc  25407  itg2splitlem  25705  mdegmullem  26039  atans2  26897  leibpilem2  26907  leibpi  26908  wilthlem2  27035  lgsdir2  27297  2lgslem3  27371  nosepdmlem  27651  ltsrec  27797  om2noseqf1o  28297  elnnzs  28397  ragncol  28781  opptgdim2  28817  hlpasch  28828  trgcopy  28876  cgrg3col4  28925  structiedg0val  29095  usgredg2v  29300  nb3grprlem2  29454  vtxd0nedgb  29562  1egrvtxdg0  29585  wwlksnndef  29978  nfrgr2v  30347  nonbooli  31726  cvnbtwn4  32364  chirredi  32469  atcvat4i  32472  nelun  32588  hashxpe  32887  domnmuln0rd  33356  lindssn  33459  ssdifidlprm  33539  mxidlirred  33553  bnj1304  34975  bnj1417  35197  erdszelem9  35393  satf0n0  35572  fmlaomn0  35584  fmla0disjsuc  35592  fmlasucdisj  35593  3orit  35910  dfon3  36084  dfrdg4  36145  weiunpo  36659  wl-df3maxtru1  37697  poimirlem18  37839  poimirlem21  37842  orsild  38289  orsird  38290  notornotel1  38296  cvrat4  39703  hdmaplem4  42034  mapdh9a  42049  aks6d1c5lem1  42390  redvmptabs  42615  mulltgt0d  42737  mullt0b2d  42739  sn-mullt0d  42740  dffltz  42877  fnwe2lem2  43293  dflim6  43506  ifpnot23  43719  ifpim123g  43741  ontric3g  43763  df3or2  44009  3ornot23VD  45087  ndisj2  45296  xrssre  45593  icccncfext  46131  fourierdlem42  46393  fourierdlem92  46442  salexct2  46583  nnfoctbdjlem  46699  euoreqb  47355  afvfv0bi  47398  afv2fv0  47511  ltnltne  47545  prproropf1olem4  47752  lighneallem4  47856  oddprmALTV  47933  usgrexmpl2trifr  48283  2itscp  49027  fucofvalne  49570