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  4236  prneimg2  4822  prnebg  4823  sotrieq2  5581  somo  5588  dflim3  7826  frxp  8108  poxp  8110  soxp  8111  frxp2  8126  frxp3  8133  suppofssd  8185  oalimcl  8527  omlimcl  8545  oeeulem  8568  fsetexb  8840  domunfican  9279  infsupprpr  9464  ordtypelem7  9484  cantnfp1lem2  9639  cantnfp1lem3  9640  cantnflem1  9649  cnfcom2lem  9661  ssfin4  10270  fin1a2lem7  10366  fin1a2lem12  10371  fpwwe2lem12  10602  fpwwe2  10603  r1wunlim  10697  recgt0  12035  elnnz  12546  xrltlen  13113  xaddf  13191  xmullem  13231  xmullem2  13232  ssfzoulel  13728  elfznelfzo  13740  elfznelfzob  13741  om2uzf1oi  13925  fsuppmapnn0fiubex  13964  bcval4  14279  sadcaddlem  16434  lcmcllem  16573  lcmgcdlem  16583  lcmftp  16613  lcmfunsnlem2lem1  16615  lcmfunsnlem2lem2  16616  lcmfunsnlem2  16617  isprm3  16660  prmdvdsbc  16703  prm23ge5  16793  pcpremul  16821  mndpsuppss  18699  subgmulg  19079  isnirred  20336  isdomn2OLD  20628  cnfldfun  21285  cnfldfunOLD  21298  mdetunilem7  22512  mndifsplit  22530  ordtbaslem  23082  iunconn  23322  fbun  23734  fin1aufil  23826  reconnlem2  24723  rrxmvallem  25311  pmltpc  25358  itg2splitlem  25656  mdegmullem  25990  atans2  26848  leibpilem2  26858  leibpi  26859  wilthlem2  26986  lgsdir2  27248  2lgslem3  27322  nosepdmlem  27602  sltrec  27739  om2noseqf1o  28202  elnnzs  28296  ragncol  28643  opptgdim2  28679  hlpasch  28690  trgcopy  28738  cgrg3col4  28787  structiedg0val  28956  usgredg2v  29161  nb3grprlem2  29315  vtxd0nedgb  29423  1egrvtxdg0  29446  wwlksnndef  29842  nfrgr2v  30208  nonbooli  31587  cvnbtwn4  32225  chirredi  32330  atcvat4i  32333  nelun  32449  hashxpe  32739  domnmuln0rd  33232  lindssn  33356  ssdifidlprm  33436  mxidlirred  33450  bnj1304  34816  bnj1417  35038  erdszelem9  35193  satf0n0  35372  fmlaomn0  35384  fmla0disjsuc  35392  fmlasucdisj  35393  3orit  35710  dfon3  35887  dfrdg4  35946  weiunpo  36460  wl-df3maxtru1  37487  poimirlem18  37639  poimirlem21  37642  orsild  38089  orsird  38090  notornotel1  38096  cvrat4  39444  hdmaplem4  41775  mapdh9a  41790  aks6d1c5lem1  42131  redvmptabs  42355  mulltgt0d  42477  mullt0b2d  42479  sn-mullt0d  42480  dffltz  42629  fnwe2lem2  43047  dflim6  43260  ifpnot23  43474  ifpim123g  43496  ontric3g  43518  df3or2  43764  3ornot23VD  44843  ndisj2  45052  xrssre  45351  icccncfext  45892  fourierdlem42  46154  fourierdlem92  46203  salexct2  46344  nnfoctbdjlem  46460  euoreqb  47114  afvfv0bi  47157  afv2fv0  47270  ltnltne  47304  prproropf1olem4  47511  lighneallem4  47615  oddprmALTV  47692  usgrexmpl2trifr  48032  2itscp  48774  fucofvalne  49318