Theorem ioran 999

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 410	. 2 ⊢ (¬ (¬ 𝜑 → 𝜓) ↔ (¬ 𝜑 ∧ ¬ 𝜓))
2		pm4.64 862	. 2 ⊢ ((¬ 𝜑 → 𝜓) ↔ (𝜑 ∨ 𝜓))
3	1, 2	xchnxbi 335	1 ⊢ (¬ (𝜑 ∨ 𝜓) ↔ (¬ 𝜑 ∧ ¬ 𝜓))

Syntax hints:  ¬ wn 3   → wi 4   ↔ wb 209   ∧ wa 400   ∨ wo 860

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 210  df-an 401  df-or 861

This theorem is referenced by:  pm4.56  1004  orsild  1019  orsird  1020  xor  1032  3ioran  1123  3ori  1451  ecase23d  1503  ecase33d  1504  19.43OLD  1913  dfun2  4223  prneimg2  4820  prnebg  4821  sotrieq2  5601  somo  5608  dflim3  7839  frxp  8118  poxp  8120  soxp  8121  frxp2  8136  frxp3  8143  suppofssd  8195  oalimcl  8541  omlimcl  8559  oeeulem  8583  fsetexb  8857  domunfican  9277  infsupprpr  9462  ordtypelem7  9482  cantnfp1lem2  9644  cantnfp1lem3  9645  cantnflem1  9654  cnfcom2lem  9666  ssfin4  10289  fin1a2lem7  10385  fin1a2lem12  10390  fpwwe2lem12  10622  fpwwe2  10623  r1wunlim  10717  recgt0  12056  elnnz  12596  xrltlen  13166  xaddf  13245  xmullem  13285  xmullem2  13286  ssfzoulel  13785  elfznelfzo  13798  elfznelfzob  13799  om2uzf1oi  13985  fsuppmapnn0fiubex  14024  bcval4  14339  sadcaddlem  16510  lcmcllem  16649  lcmgcdlem  16659  lcmftp  16689  lcmfunsnlem2lem1  16691  lcmfunsnlem2lem2  16692  lcmfunsnlem2  16693  isprm3  16736  prmdvdsbc  16780  prm23ge5  16870  pcpremul  16898  mndpsuppss  18818  subgmulg  19202  isnirred  20498  ssdifidlprm  21486  prmidlsubm  21487  cnfldfun  21536  mdetunilem7  22775  mndifsplit  22793  ordtbaslem  23345  iunconn  23585  fbun  23997  fin1aufil  24089  reconnlem2  24985  rrxmvallem  25563  pmltpc  25609  itg2splitlem  25907  mdegmullem  26235  atans2  27096  leibpilem2  27106  leibpi  27107  wilthlem2  27233  lgsdir2  27494  2lgslem3  27568  nosepdmlem  27847  ltsrec  27994  om2noseqf1o  28494  elnnzs  28594  ragncol  28989  opptgdim2  29026  hlpasch  29038  trgcopy  29115  cgrg3col4  29170  prlngex  29201  prlngmid2  29211  tgaltai  29217  structiedg0val  29372  usgredg2v  29577  nb3grprlem2  29731  vtxd0nedgb  29838  1egrvtxdg0  29861  wwlksnndef  30254  nfrgr2v  30623  nonbooli  32003  cvnbtwn4  32641  chirredi  32746  atcvat4i  32749  nelun  32859  hashxpe  33152  domnmuln0rd  33597  lindssn  33691  mxidlirred  33755  dflringlem2  33785  morleylemrneab  35058  bnj1304  35207  bnj1417  35429  erdszelem9  35691  satf0n0  35870  fmlaomn0  35882  fmla0disjsuc  35890  fmlasucdisj  35891  3orit  36208  dfon3  36382  dfrdg4  36443  weiunpo  36976  wl-df3maxtru1  38138  poimirlem18  38289  poimirlem21  38292  notornotel1  38744  cvrat4  40217  hdmaplem4  42548  mapdh9a  42563  aks6d1c5lem1  42903  redvmptabs  43121  mulltgt0d  43256  mullt0b2d  43258  sn-mullt0d  43259  dffltz  43366  fnwe2lem2  43778  dflim6  43991  ifpnot23  44204  ifpim123g  44226  ontric3g  44248  df3or2  44494  3ornot23VD  45555  ndisj2  45771  xrssre  46064  icccncfext  46601  fourierdlem42  46863  fourierdlem92  46912  salexct2  47053  nnfoctbdjlem  47169  euoreqb  47846  afvfv0bi  47889  afv2fv0  48002  ltnltne  48036  prproropf1olem4  48255  lighneallem4  48362  oddprmALTV  48452  usgrexmpl2trifr  48802  2itscp  49561  fucofvalne  50103