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  1427  ecase23d  1476  19.43OLD  1885  dfun2  4211  prneimg2  4799  prnebg  4800  sotrieq2  5564  somo  5571  dflim3  7791  frxp  8069  poxp  8071  soxp  8072  frxp2  8087  frxp3  8094  suppofssd  8146  oalimcl  8488  omlimcl  8506  oeeulem  8530  fsetexb  8804  domunfican  9225  infsupprpr  9412  ordtypelem7  9432  cantnfp1lem2  9591  cantnfp1lem3  9592  cantnflem1  9601  cnfcom2lem  9613  ssfin4  10223  fin1a2lem7  10319  fin1a2lem12  10324  fpwwe2lem12  10556  fpwwe2  10557  r1wunlim  10651  recgt0  11992  elnnz  12525  xrltlen  13088  xaddf  13167  xmullem  13207  xmullem2  13208  ssfzoulel  13706  elfznelfzo  13719  elfznelfzob  13720  om2uzf1oi  13906  fsuppmapnn0fiubex  13945  bcval4  14260  sadcaddlem  16417  lcmcllem  16556  lcmgcdlem  16566  lcmftp  16596  lcmfunsnlem2lem1  16598  lcmfunsnlem2lem2  16599  lcmfunsnlem2  16600  isprm3  16643  prmdvdsbc  16687  prm23ge5  16777  pcpremul  16805  mndpsuppss  18724  subgmulg  19107  isnirred  20391  isdomn2OLD  20680  cnfldfun  21358  cnfldfunOLD  21371  mdetunilem7  22593  mndifsplit  22611  ordtbaslem  23163  iunconn  23403  fbun  23815  fin1aufil  23907  reconnlem2  24803  rrxmvallem  25381  pmltpc  25427  itg2splitlem  25725  mdegmullem  26053  atans2  26908  leibpilem2  26918  leibpi  26919  wilthlem2  27046  lgsdir2  27307  2lgslem3  27381  nosepdmlem  27661  ltsrec  27807  om2noseqf1o  28307  elnnzs  28407  ragncol  28791  opptgdim2  28827  hlpasch  28838  trgcopy  28886  cgrg3col4  28935  structiedg0val  29105  usgredg2v  29310  nb3grprlem2  29464  vtxd0nedgb  29572  1egrvtxdg0  29595  wwlksnndef  29988  nfrgr2v  30357  nonbooli  31737  cvnbtwn4  32375  chirredi  32480  atcvat4i  32483  nelun  32598  hashxpe  32895  domnmuln0rd  33350  lindssn  33453  ssdifidlprm  33533  mxidlirred  33547  bnj1304  34977  bnj1417  35199  erdszelem9  35397  satf0n0  35576  fmlaomn0  35588  fmla0disjsuc  35596  fmlasucdisj  35597  3orit  35914  dfon3  36088  dfrdg4  36149  weiunpo  36663  wl-df3maxtru1  37822  poimirlem18  37973  poimirlem21  37976  orsild  38423  orsird  38424  notornotel1  38430  cvrat4  39903  hdmaplem4  42234  mapdh9a  42249  aks6d1c5lem1  42589  redvmptabs  42806  mulltgt0d  42941  mullt0b2d  42943  sn-mullt0d  42944  dffltz  43081  fnwe2lem2  43497  dflim6  43710  ifpnot23  43923  ifpim123g  43945  ontric3g  43967  df3or2  44213  3ornot23VD  45291  ndisj2  45500  xrssre  45796  icccncfext  46333  fourierdlem42  46595  fourierdlem92  46644  salexct2  46785  nnfoctbdjlem  46901  euoreqb  47569  afvfv0bi  47612  afv2fv0  47725  ltnltne  47759  prproropf1olem4  47978  lighneallem4  48085  oddprmALTV  48175  usgrexmpl2trifr  48525  2itscp  49269  fucofvalne  49812