Theorem ioran 986

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

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

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 849

This theorem is referenced by:  pm4.56  991  xor  1017  3ioran  1106  3ori  1427  ecase23d  1476  19.43OLD  1885  dfun2  4224  prneimg2  4813  prnebg  4814  sotrieq2  5572  somo  5579  dflim3  7799  frxp  8078  poxp  8080  soxp  8081  frxp2  8096  frxp3  8103  suppofssd  8155  oalimcl  8497  omlimcl  8515  oeeulem  8539  fsetexb  8813  domunfican  9234  infsupprpr  9421  ordtypelem7  9441  cantnfp1lem2  9600  cantnfp1lem3  9601  cantnflem1  9610  cnfcom2lem  9622  ssfin4  10232  fin1a2lem7  10328  fin1a2lem12  10333  fpwwe2lem12  10565  fpwwe2  10566  r1wunlim  10660  recgt0  11999  elnnz  12510  xrltlen  13072  xaddf  13151  xmullem  13191  xmullem2  13192  ssfzoulel  13688  elfznelfzo  13701  elfznelfzob  13702  om2uzf1oi  13888  fsuppmapnn0fiubex  13927  bcval4  14242  sadcaddlem  16396  lcmcllem  16535  lcmgcdlem  16545  lcmftp  16575  lcmfunsnlem2lem1  16577  lcmfunsnlem2lem2  16578  lcmfunsnlem2  16579  isprm3  16622  prmdvdsbc  16665  prm23ge5  16755  pcpremul  16783  mndpsuppss  18702  subgmulg  19082  isnirred  20368  isdomn2OLD  20657  cnfldfun  21335  cnfldfunOLD  21348  mdetunilem7  22574  mndifsplit  22592  ordtbaslem  23144  iunconn  23384  fbun  23796  fin1aufil  23888  reconnlem2  24784  rrxmvallem  25372  pmltpc  25419  itg2splitlem  25717  mdegmullem  26051  atans2  26909  leibpilem2  26919  leibpi  26920  wilthlem2  27047  lgsdir2  27309  2lgslem3  27383  nosepdmlem  27663  ltsrec  27809  om2noseqf1o  28309  elnnzs  28409  ragncol  28793  opptgdim2  28829  hlpasch  28840  trgcopy  28888  cgrg3col4  28937  structiedg0val  29107  usgredg2v  29312  nb3grprlem2  29466  vtxd0nedgb  29574  1egrvtxdg0  29597  wwlksnndef  29990  nfrgr2v  30359  nonbooli  31739  cvnbtwn4  32377  chirredi  32482  atcvat4i  32485  nelun  32600  hashxpe  32898  domnmuln0rd  33368  lindssn  33471  ssdifidlprm  33551  mxidlirred  33565  bnj1304  34995  bnj1417  35217  erdszelem9  35415  satf0n0  35594  fmlaomn0  35606  fmla0disjsuc  35614  fmlasucdisj  35615  3orit  35932  dfon3  36106  dfrdg4  36167  weiunpo  36681  wl-df3maxtru1  37747  poimirlem18  37889  poimirlem21  37892  orsild  38339  orsird  38340  notornotel1  38346  cvrat4  39819  hdmaplem4  42150  mapdh9a  42165  aks6d1c5lem1  42506  redvmptabs  42730  mulltgt0d  42852  mullt0b2d  42854  sn-mullt0d  42855  dffltz  42992  fnwe2lem2  43408  dflim6  43621  ifpnot23  43834  ifpim123g  43856  ontric3g  43878  df3or2  44124  3ornot23VD  45202  ndisj2  45411  xrssre  45707  icccncfext  46245  fourierdlem42  46507  fourierdlem92  46556  salexct2  46697  nnfoctbdjlem  46813  euoreqb  47469  afvfv0bi  47512  afv2fv0  47625  ltnltne  47659  prproropf1olem4  47866  lighneallem4  47970  oddprmALTV  48047  usgrexmpl2trifr  48397  2itscp  49141  fucofvalne  49684