Theorem ioran 982

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

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

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 206  df-an 396  df-or 847

This theorem is referenced by:  pm4.56  987  xor  1013  3ioran  1104  3ori  1422  ecase23d  1470  19.43OLD  1879  2ralorOLD  3226  dfun2  4260  prnebg  4857  sotrieq2  5620  somo  5627  dflim3  7851  frxp  8131  poxp  8133  soxp  8134  frxp2  8149  frxp3  8156  suppofssd  8209  oalimcl  8581  omlimcl  8599  oeeulem  8622  fsetexb  8883  domunfican  9345  infsupprpr  9528  ordtypelem7  9548  cantnfp1lem2  9703  cantnfp1lem3  9704  cantnflem1  9713  cnfcom2lem  9725  ssfin4  10334  fin1a2lem7  10430  fin1a2lem12  10435  fpwwe2lem12  10666  fpwwe2  10667  r1wunlim  10761  1re  11245  recgt0  12091  elnnz  12599  xrltlen  13158  xaddf  13236  xmullem  13276  xmullem2  13277  ssfzoulel  13759  elfznelfzo  13770  elfznelfzob  13771  om2uzf1oi  13951  fsuppmapnn0fiubex  13990  bcval4  14299  sadcaddlem  16432  lcmcllem  16567  lcmgcdlem  16577  lcmftp  16607  lcmfunsnlem2lem1  16609  lcmfunsnlem2lem2  16610  lcmfunsnlem2  16611  isprm3  16654  prmdvdsbc  16698  prm23ge5  16784  pcpremul  16812  subgmulg  19095  isnirred  20359  isdomn2  21246  cnfldfun  21293  cnfldfunOLD  21306  mdetunilem7  22533  mndifsplit  22551  ordtbaslem  23105  iunconn  23345  fbun  23757  fin1aufil  23849  reconnlem2  24756  rrxmvallem  25345  pmltpc  25392  itg2splitlem  25691  mdegmullem  26027  atans2  26876  leibpilem2  26886  leibpi  26887  wilthlem2  27014  lgsdir2  27276  2lgslem3  27350  nosepdmlem  27629  sltrec  27766  om2noseqf1o  28187  ragncol  28526  opptgdim2  28562  hlpasch  28573  trgcopy  28621  cgrg3col4  28670  structiedg0val  28848  usgredg2v  29053  nb3grprlem2  29207  vtxd0nedgb  29315  1egrvtxdg0  29338  wwlksnndef  29729  nfrgr2v  30095  nonbooli  31474  cvnbtwn4  32112  chirredi  32217  atcvat4i  32220  nelun  32322  hashxpe  32589  lindssn  33106  mxidlirred  33198  bnj1304  34450  bnj1417  34672  erdszelem9  34809  satf0n0  34988  fmlaomn0  35000  fmla0disjsuc  35008  fmlasucdisj  35009  3orit  35310  dfon3  35488  dfrdg4  35547  wl-df3maxtru1  36971  poimirlem18  37111  poimirlem21  37114  orsild  37561  orsird  37562  notornotel1  37568  cvrat4  38916  hdmaplem4  41247  mapdh9a  41262  aks6d1c5lem1  41607  metakunt12  41668  dffltz  42058  fnwe2lem2  42475  dflim6  42693  ifpnot23  42908  ifpim123g  42930  ontric3g  42952  df3or2  43198  3ornot23VD  44286  ndisj2  44415  xrssre  44730  icccncfext  45275  fourierdlem42  45537  fourierdlem92  45586  salexct2  45727  nnfoctbdjlem  45843  euoreqb  46489  afvfv0bi  46532  afv2fv0  46645  ltnltne  46679  prproropf1olem4  46846  lighneallem4  46950  oddprmALTV  47027  mndpsuppss  47435  2itscp  47854

Otomatik - 173.255.232.114 CloudFlare DNS Türk Telekom DNS Google DNS Open DNS

OSZAR »