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  1426  ecase23d  1475  19.43OLD  1883  2ralorOLD  3232  dfun2  4270  prneimg2  4855  prnebg  4856  sotrieq2  5624  somo  5631  dflim3  7868  frxp  8151  poxp  8153  soxp  8154  frxp2  8169  frxp3  8176  suppofssd  8228  oalimcl  8598  omlimcl  8616  oeeulem  8639  fsetexb  8904  domunfican  9361  infsupprpr  9544  ordtypelem7  9564  cantnfp1lem2  9719  cantnfp1lem3  9720  cantnflem1  9729  cnfcom2lem  9741  ssfin4  10350  fin1a2lem7  10446  fin1a2lem12  10451  fpwwe2lem12  10682  fpwwe2  10683  r1wunlim  10777  1re  11261  recgt0  12113  elnnz  12623  xrltlen  13188  xaddf  13266  xmullem  13306  xmullem2  13307  ssfzoulel  13799  elfznelfzo  13811  elfznelfzob  13812  om2uzf1oi  13994  fsuppmapnn0fiubex  14033  bcval4  14346  sadcaddlem  16494  lcmcllem  16633  lcmgcdlem  16643  lcmftp  16673  lcmfunsnlem2lem1  16675  lcmfunsnlem2lem2  16676  lcmfunsnlem2  16677  isprm3  16720  prmdvdsbc  16763  prm23ge5  16853  pcpremul  16881  mndpsuppss  18778  subgmulg  19158  isnirred  20420  isdomn2OLD  20712  cnfldfun  21378  cnfldfunOLD  21391  mdetunilem7  22624  mndifsplit  22642  ordtbaslem  23196  iunconn  23436  fbun  23848  fin1aufil  23940  reconnlem2  24849  rrxmvallem  25438  pmltpc  25485  itg2splitlem  25783  mdegmullem  26117  atans2  26974  leibpilem2  26984  leibpi  26985  wilthlem2  27112  lgsdir2  27374  2lgslem3  27448  nosepdmlem  27728  sltrec  27865  om2noseqf1o  28307  elnnzs  28387  ragncol  28717  opptgdim2  28753  hlpasch  28764  trgcopy  28812  cgrg3col4  28861  structiedg0val  29039  usgredg2v  29244  nb3grprlem2  29398  vtxd0nedgb  29506  1egrvtxdg0  29529  wwlksnndef  29925  nfrgr2v  30291  nonbooli  31670  cvnbtwn4  32308  chirredi  32413  atcvat4i  32416  nelun  32532  hashxpe  32811  domnmuln0rd  33278  lindssn  33406  ssdifidlprm  33486  mxidlirred  33500  bnj1304  34833  bnj1417  35055  erdszelem9  35204  satf0n0  35383  fmlaomn0  35395  fmla0disjsuc  35403  fmlasucdisj  35404  3orit  35716  dfon3  35893  dfrdg4  35952  weiunpo  36466  wl-df3maxtru1  37493  poimirlem18  37645  poimirlem21  37648  orsild  38095  orsird  38096  notornotel1  38102  cvrat4  39445  hdmaplem4  41776  mapdh9a  41791  aks6d1c5lem1  42137  metakunt12  42217  redvmptabs  42390  dffltz  42644  fnwe2lem2  43063  dflim6  43277  ifpnot23  43491  ifpim123g  43513  ontric3g  43535  df3or2  43781  3ornot23VD  44867  ndisj2  45056  xrssre  45359  icccncfext  45902  fourierdlem42  46164  fourierdlem92  46213  salexct2  46354  nnfoctbdjlem  46470  euoreqb  47121  afvfv0bi  47164  afv2fv0  47277  ltnltne  47311  prproropf1olem4  47493  lighneallem4  47597  oddprmALTV  47674  usgrexmpl2trifr  47996  2itscp  48702  fucofvalne  49020