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

This proof depends on syntax axioms:  ¬ wn 3   → wi 4   ↔ wb 209   ∧ wa 401   ∨ wo 861

This proof depends on axioms:  ax-mp 5  ax-1 6  ax-2 7  ax-3 8

This proof depends on definitions:  df-bi 210  df-an 402  df-or 862

This theorem is used by:  pm4.56  1004  orsild  1019  orsird  1020  xor  1032  3ioran  1123  3ori  1451  ecase23d  1503  ecase33d  1504  19.43OLD  1915  dfun2  4214  prneimg2  4809  prnebg  4810  sotrieq2  5590  somo  5597  dflim3  7860  frxp  8142  poxp  8144  soxp  8145  fnwe2lem3  8151  frxp2  8165  frxp3  8172  suppofssd  8225  oalimcl  8573  omlimcl  8591  oeeulem  8615  fsetexb  8891  domunfican  9318  infsupprpr  9503  ordtypelem7  9523  cantnfp1lem2  9685  cantnfp1lem3  9686  cantnflem1  9695  cnfcom2lem  9707  ssfin4  10393  fin1a2lem7  10489  fin1a2lem12  10494  fpwwe2lem12  10732  fpwwe2  10733  r1wunlim  10827  recgt0  12168  elnnz  12708  xrltlen  13280  xaddf  13359  xmullem  13399  xmullem2  13400  ssfzoulel  13900  elfznelfzo  13913  elfznelfzob  13914  om2uzf1oi  14101  fsuppmapnn0fiubex  14140  bcval4  14456  sadcaddlem  16634  lcmcllem  16778  lcmgcdlem  16788  lcmftp  16818  lcmfunsnlem2lem1  16820  lcmfunsnlem2lem2  16821  lcmfunsnlem2  16822  isprm3  16865  prmdvdsbc  16909  prm23ge5  17000  pcpremul  17028  mndpsuppss  18966  subgmulg  19358  isnirred  20657  ssdifidlprm  21649  prmidlsubm  21650  cnfldfun  21699  mdetunilem7  22940  mndifsplit  22958  ordtbaslem  23513  iunconn  23753  fbun  24166  fin1aufil  24258  reconnlem2  25154  rrxmvallem  25732  pmltpc  25778  itg2splitlem  26076  mdegmullem  26403  atans2  27266  leibpilem2  27276  leibpi  27277  wilthlem2  27403  lgsdir2  27664  2lgslem3  27738  nosepdmlem  28047  ltsrec  28194  om2noseqf1o  28694  elnnzs  28794  ragncol  29191  opptgdim2  29228  hlpasch  29241  trgcopy  29318  tgaaddcpbllem1  29356  tgaaddcpbl  29359  cgrg3col4  29379  angmgmaddeu1  29386  angmgmaddcpbl  29397  prlngex  29436  prlngmid2  29446  tgaltai  29452  structiedg0val  29607  usgredg2v  29815  nb3grprlem2  29969  vtxd0nedgb  30076  1egrvtxdg0  30099  wwlksnndef  30501  nfrgr2v  30880  nonbooli  32260  cvnbtwn4  32898  chirredi  33003  atcvat4i  33006  inagcgrabtwn  33058  tgextamirn  33074  tgextancd  33075  tgextalem1inag  33077  tgextamirnhl  33079  tgextancgra  33081  nelun  33158  hashxpe  33447  domnmuln0rd  33886  lindssn  33981  mxidlirred  34045  dflringlem2  34075  morleylemrneab  35348  bnj1304  35497  bnj1417  35719  erdszelem9  36052  satf0n0  36231  fmlaomn0  36243  fmla0disjsuc  36251  fmlasucdisj  36252  3orit  36575  dfon3  36748  dfrdg4  36809  weiunpo  37347  wl-df3maxtru1  38522  poimirlem18  38663  poimirlem21  38666  notornotel1  39134  cvrat4  40607  hdmaplem4  42938  mapdh9a  42953  aks6d1c5lem1  43293  redvmptabs  43518  mulltgt0d  43653  mullt0b2d  43655  sn-mullt0d  43656  dffltz  43777  dflim6  44373  ifpnot23  44586  ifpim123g  44608  ontric3g  44630  df3or2  44875  3ornot23VD  45936  ndisj2  46175  xrssre  46467  icccncfext  47004  fourierdlem42  47266  fourierdlem92  47315  salexct2  47456  nnfoctbdjlem  47572  euoreqb  48286  afvfv0bi  48329  afv2fv0  48442  ltnltne  48476  prproropf1olem4  48695  lighneallem4  48802  oddprmALTV  48892  usgrexmpl2trifr  49242  2itscp  50000  fucofvalne  50554