Theorem ioran 991

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

Syntax hints:  ¬ wn 3   → wi 4   ↔ wb 207   ∧ wa 396   ∨ wo 853

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 208  df-an 397  df-or 854

This theorem is referenced by:  pm4.56  996  xor  1022  3ioran  1111  3ori  1432  ecase23d  1481  19.43OLD  1890  dfun2  4198  prneimg2  4786  prnebg  4787  sotrieq2  5558  somo  5565  dflim3  7787  frxp  8066  poxp  8068  soxp  8069  frxp2  8084  frxp3  8091  suppofssd  8143  oalimcl  8485  omlimcl  8503  oeeulem  8527  fsetexb  8801  domunfican  9222  infsupprpr  9409  ordtypelem7  9429  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  20684  cnfldfun  21361  mdetunilem7  22601  mndifsplit  22619  ordtbaslem  23171  iunconn  23411  fbun  23823  fin1aufil  23915  reconnlem2  24811  rrxmvallem  25389  pmltpc  25435  itg2splitlem  25733  mdegmullem  26061  atans2  26913  leibpilem2  26923  leibpi  26924  wilthlem2  27050  lgsdir2  27311  2lgslem3  27385  nosepdmlem  27665  ltsrec  27811  om2noseqf1o  28311  elnnzs  28411  ragncol  28795  opptgdim2  28831  hlpasch  28842  trgcopy  28890  cgrg3col4  28939  structiedg0val  29109  usgredg2v  29314  nb3grprlem2  29468  vtxd0nedgb  29575  1egrvtxdg0  29598  wwlksnndef  29991  nfrgr2v  30360  nonbooli  31740  cvnbtwn4  32378  chirredi  32483  atcvat4i  32486  nelun  32601  hashxpe  32899  domnmuln0rd  33355  lindssn  33461  ssdifidlprm  33541  mxidlirred  33555  bnj1304  35001  bnj1417  35223  erdszelem9  35427  satf0n0  35606  fmlaomn0  35618  fmla0disjsuc  35626  fmlasucdisj  35627  3orit  35944  dfon3  36118  dfrdg4  36179  weiunpo  36693  wl-df3maxtru1  37854  poimirlem18  38005  poimirlem21  38008  orsild  38455  orsird  38456  notornotel1  38462  cvrat4  39935  hdmaplem4  42266  mapdh9a  42281  aks6d1c5lem1  42621  redvmptabs  42837  mulltgt0d  42972  mullt0b2d  42974  sn-mullt0d  42975  dffltz  43084  fnwe2lem2  43496  dflim6  43709  ifpnot23  43922  ifpim123g  43944  ontric3g  43966  df3or2  44212  3ornot23VD  45290  ndisj2  45499  xrssre  45793  icccncfext  46330  fourierdlem42  46592  fourierdlem92  46641  salexct2  46782  nnfoctbdjlem  46898  euoreqb  47572  afvfv0bi  47615  afv2fv0  47728  ltnltne  47762  prproropf1olem4  47981  lighneallem4  48088  oddprmALTV  48178  usgrexmpl2trifr  48528  2itscp  49272  fucofvalne  49815