Theorem ioran 985

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 849	. 2 ⊢ ((¬ 𝜑 → 𝜓) ↔ (𝜑 ∨ 𝜓))
3	1, 2	xchnxbi 332	1 ⊢ (¬ (𝜑 ∨ 𝜓) ↔ (¬ 𝜑 ∧ ¬ 𝜓))

Syntax hints:  ¬ wn 3   → wi 4   ↔ wb 206   ∧ wa 395   ∨ wo 847

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 848

This theorem is referenced by:  pm4.56  990  xor  1016  3ioran  1105  3ori  1426  ecase23d  1475  19.43OLD  1883  dfun2  4233  prneimg2  4819  prnebg  4820  sotrieq2  5578  somo  5585  dflim3  7823  frxp  8105  poxp  8107  soxp  8108  frxp2  8123  frxp3  8130  suppofssd  8182  oalimcl  8524  omlimcl  8542  oeeulem  8565  fsetexb  8837  domunfican  9272  infsupprpr  9457  ordtypelem7  9477  cantnfp1lem2  9632  cantnfp1lem3  9633  cantnflem1  9642  cnfcom2lem  9654  ssfin4  10263  fin1a2lem7  10359  fin1a2lem12  10364  fpwwe2lem12  10595  fpwwe2  10596  r1wunlim  10690  recgt0  12028  elnnz  12539  xrltlen  13106  xaddf  13184  xmullem  13224  xmullem2  13225  ssfzoulel  13721  elfznelfzo  13733  elfznelfzob  13734  om2uzf1oi  13918  fsuppmapnn0fiubex  13957  bcval4  14272  sadcaddlem  16427  lcmcllem  16566  lcmgcdlem  16576  lcmftp  16606  lcmfunsnlem2lem1  16608  lcmfunsnlem2lem2  16609  lcmfunsnlem2  16610  isprm3  16653  prmdvdsbc  16696  prm23ge5  16786  pcpremul  16814  mndpsuppss  18692  subgmulg  19072  isnirred  20329  isdomn2OLD  20621  cnfldfun  21278  cnfldfunOLD  21291  mdetunilem7  22505  mndifsplit  22523  ordtbaslem  23075  iunconn  23315  fbun  23727  fin1aufil  23819  reconnlem2  24716  rrxmvallem  25304  pmltpc  25351  itg2splitlem  25649  mdegmullem  25983  atans2  26841  leibpilem2  26851  leibpi  26852  wilthlem2  26979  lgsdir2  27241  2lgslem3  27315  nosepdmlem  27595  sltrec  27732  om2noseqf1o  28195  elnnzs  28289  ragncol  28636  opptgdim2  28672  hlpasch  28683  trgcopy  28731  cgrg3col4  28780  structiedg0val  28949  usgredg2v  29154  nb3grprlem2  29308  vtxd0nedgb  29416  1egrvtxdg0  29439  wwlksnndef  29835  nfrgr2v  30201  nonbooli  31580  cvnbtwn4  32218  chirredi  32323  atcvat4i  32326  nelun  32442  hashxpe  32732  domnmuln0rd  33225  lindssn  33349  ssdifidlprm  33429  mxidlirred  33443  bnj1304  34809  bnj1417  35031  erdszelem9  35186  satf0n0  35365  fmlaomn0  35377  fmla0disjsuc  35385  fmlasucdisj  35386  3orit  35703  dfon3  35880  dfrdg4  35939  weiunpo  36453  wl-df3maxtru1  37480  poimirlem18  37632  poimirlem21  37635  orsild  38082  orsird  38083  notornotel1  38089  cvrat4  39437  hdmaplem4  41768  mapdh9a  41783  aks6d1c5lem1  42124  redvmptabs  42348  mulltgt0d  42470  mullt0b2d  42472  sn-mullt0d  42473  dffltz  42622  fnwe2lem2  43040  dflim6  43253  ifpnot23  43467  ifpim123g  43489  ontric3g  43511  df3or2  43757  3ornot23VD  44836  ndisj2  45045  xrssre  45344  icccncfext  45885  fourierdlem42  46147  fourierdlem92  46196  salexct2  46337  nnfoctbdjlem  46453  euoreqb  47110  afvfv0bi  47153  afv2fv0  47266  ltnltne  47300  prproropf1olem4  47507  lighneallem4  47611  oddprmALTV  47688  usgrexmpl2trifr  48028  2itscp  48770  fucofvalne  49314