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  4217  prneimg2  4804  prnebg  4805  sotrieq2  5553  somo  5560  dflim3  7771  frxp  8050  poxp  8052  soxp  8053  frxp2  8068  frxp3  8075  suppofssd  8127  oalimcl  8469  omlimcl  8487  oeeulem  8510  fsetexb  8782  domunfican  9200  infsupprpr  9384  ordtypelem7  9404  cantnfp1lem2  9563  cantnfp1lem3  9564  cantnflem1  9573  cnfcom2lem  9585  ssfin4  10192  fin1a2lem7  10288  fin1a2lem12  10293  fpwwe2lem12  10524  fpwwe2  10525  r1wunlim  10619  recgt0  11958  elnnz  12469  xrltlen  13036  xaddf  13114  xmullem  13154  xmullem2  13155  ssfzoulel  13651  elfznelfzo  13663  elfznelfzob  13664  om2uzf1oi  13848  fsuppmapnn0fiubex  13887  bcval4  14202  sadcaddlem  16355  lcmcllem  16494  lcmgcdlem  16504  lcmftp  16534  lcmfunsnlem2lem1  16536  lcmfunsnlem2lem2  16537  lcmfunsnlem2  16538  isprm3  16581  prmdvdsbc  16624  prm23ge5  16714  pcpremul  16742  mndpsuppss  18626  subgmulg  19006  isnirred  20292  isdomn2OLD  20581  cnfldfun  21259  cnfldfunOLD  21272  mdetunilem7  22487  mndifsplit  22505  ordtbaslem  23057  iunconn  23297  fbun  23709  fin1aufil  23801  reconnlem2  24697  rrxmvallem  25285  pmltpc  25332  itg2splitlem  25630  mdegmullem  25964  atans2  26822  leibpilem2  26832  leibpi  26833  wilthlem2  26960  lgsdir2  27222  2lgslem3  27296  nosepdmlem  27576  sltrec  27716  om2noseqf1o  28185  elnnzs  28279  ragncol  28641  opptgdim2  28677  hlpasch  28688  trgcopy  28736  cgrg3col4  28785  structiedg0val  28954  usgredg2v  29159  nb3grprlem2  29313  vtxd0nedgb  29421  1egrvtxdg0  29444  wwlksnndef  29837  nfrgr2v  30203  nonbooli  31582  cvnbtwn4  32220  chirredi  32325  atcvat4i  32328  nelun  32445  hashxpe  32744  domnmuln0rd  33209  lindssn  33311  ssdifidlprm  33391  mxidlirred  33405  bnj1304  34799  bnj1417  35021  erdszelem9  35189  satf0n0  35368  fmlaomn0  35380  fmla0disjsuc  35388  fmlasucdisj  35389  3orit  35706  dfon3  35883  dfrdg4  35942  weiunpo  36456  wl-df3maxtru1  37483  poimirlem18  37635  poimirlem21  37638  orsild  38085  orsird  38086  notornotel1  38092  cvrat4  39439  hdmaplem4  41770  mapdh9a  41785  aks6d1c5lem1  42126  redvmptabs  42350  mulltgt0d  42472  mullt0b2d  42474  sn-mullt0d  42475  dffltz  42624  fnwe2lem2  43041  dflim6  43254  ifpnot23  43468  ifpim123g  43490  ontric3g  43512  df3or2  43758  3ornot23VD  44836  ndisj2  45045  xrssre  45344  icccncfext  45882  fourierdlem42  46144  fourierdlem92  46193  salexct2  46334  nnfoctbdjlem  46450  euoreqb  47107  afvfv0bi  47150  afv2fv0  47263  ltnltne  47297  prproropf1olem4  47504  lighneallem4  47608  oddprmALTV  47685  usgrexmpl2trifr  48035  2itscp  48780  fucofvalne  49324