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  4221  prneimg2  4806  prnebg  4807  sotrieq2  5559  somo  5566  dflim3  7780  frxp  8059  poxp  8061  soxp  8062  frxp2  8077  frxp3  8084  suppofssd  8136  oalimcl  8478  omlimcl  8496  oeeulem  8519  fsetexb  8791  domunfican  9211  infsupprpr  9396  ordtypelem7  9416  cantnfp1lem2  9575  cantnfp1lem3  9576  cantnflem1  9585  cnfcom2lem  9597  ssfin4  10204  fin1a2lem7  10300  fin1a2lem12  10305  fpwwe2lem12  10536  fpwwe2  10537  r1wunlim  10631  recgt0  11970  elnnz  12481  xrltlen  13048  xaddf  13126  xmullem  13166  xmullem2  13167  ssfzoulel  13663  elfznelfzo  13675  elfznelfzob  13676  om2uzf1oi  13860  fsuppmapnn0fiubex  13899  bcval4  14214  sadcaddlem  16368  lcmcllem  16507  lcmgcdlem  16517  lcmftp  16547  lcmfunsnlem2lem1  16549  lcmfunsnlem2lem2  16550  lcmfunsnlem2  16551  isprm3  16594  prmdvdsbc  16637  prm23ge5  16727  pcpremul  16755  mndpsuppss  18639  subgmulg  19019  isnirred  20305  isdomn2OLD  20597  cnfldfun  21275  cnfldfunOLD  21288  mdetunilem7  22503  mndifsplit  22521  ordtbaslem  23073  iunconn  23313  fbun  23725  fin1aufil  23817  reconnlem2  24714  rrxmvallem  25302  pmltpc  25349  itg2splitlem  25647  mdegmullem  25981  atans2  26839  leibpilem2  26849  leibpi  26850  wilthlem2  26977  lgsdir2  27239  2lgslem3  27313  nosepdmlem  27593  sltrec  27732  om2noseqf1o  28200  elnnzs  28294  ragncol  28654  opptgdim2  28690  hlpasch  28701  trgcopy  28749  cgrg3col4  28798  structiedg0val  28967  usgredg2v  29172  nb3grprlem2  29326  vtxd0nedgb  29434  1egrvtxdg0  29457  wwlksnndef  29850  nfrgr2v  30216  nonbooli  31595  cvnbtwn4  32233  chirredi  32338  atcvat4i  32341  nelun  32457  hashxpe  32752  domnmuln0rd  33214  lindssn  33315  ssdifidlprm  33395  mxidlirred  33409  bnj1304  34786  bnj1417  35008  erdszelem9  35172  satf0n0  35351  fmlaomn0  35363  fmla0disjsuc  35371  fmlasucdisj  35372  3orit  35689  dfon3  35866  dfrdg4  35925  weiunpo  36439  wl-df3maxtru1  37466  poimirlem18  37618  poimirlem21  37621  orsild  38068  orsird  38069  notornotel1  38075  cvrat4  39422  hdmaplem4  41753  mapdh9a  41768  aks6d1c5lem1  42109  redvmptabs  42333  mulltgt0d  42455  mullt0b2d  42457  sn-mullt0d  42458  dffltz  42607  fnwe2lem2  43024  dflim6  43237  ifpnot23  43451  ifpim123g  43473  ontric3g  43495  df3or2  43741  3ornot23VD  44820  ndisj2  45029  xrssre  45328  icccncfext  45868  fourierdlem42  46130  fourierdlem92  46179  salexct2  46320  nnfoctbdjlem  46436  euoreqb  47093  afvfv0bi  47136  afv2fv0  47249  ltnltne  47283  prproropf1olem4  47490  lighneallem4  47594  oddprmALTV  47671  usgrexmpl2trifr  48021  2itscp  48766  fucofvalne  49310