Theorem exlimddv 1945

Description: Existential elimination rule of natural deduction. (Contributed by Mario Carneiro, 15-Jun-2016.)

Hypotheses

Ref	Expression
exlimddv.1	⊢ (𝜑 → ∃𝑥𝜓)
exlimddv.2	⊢ ((𝜑 ∧ 𝜓) → 𝜒)

Assertion

Ref	Expression
exlimddv	⊢ (𝜑 → 𝜒)

Distinct variable groups:   𝜒,𝑥   𝜑,𝑥

Allowed substitution hint:   𝜓(𝑥)

Proof of Theorem exlimddv

Step	Hyp	Ref	Expression
1		exlimddv.1	. 2 ⊢ (𝜑 → ∃𝑥𝜓)
2		exlimddv.2	. . . 4 ⊢ ((𝜑 ∧ 𝜓) → 𝜒)
3	2	ex 115	. . 3 ⊢ (𝜑 → (𝜓 → 𝜒))
4	3	exlimdv 1865	. 2 ⊢ (𝜑 → (∃𝑥𝜓 → 𝜒))
5	1, 4	mpd 13	1 ⊢ (𝜑 → 𝜒)

Syntax hints:   → wi 4   ∧ wa 104  ∃wex 1538

This theorem was proved from axioms:  ax-mp 5  ax-1 6  ax-2 7  ax-ia1 106  ax-ia3 108  ax-5 1493  ax-gen 1495  ax-ie2 1540  ax-17 1572

This theorem depends on definitions:  df-bi 117

This theorem is referenced by:  fvmptdv2  5729  tfrlemi14d  6490  tfrexlem  6491  tfr1onlemres  6506  tfrcllemres  6519  tfrcldm  6520  erref  6713  en2  6986  en2m  6987  xpdom2  7003  dom0  7012  xpen  7019  mapdom1g  7021  phplem4dom  7036  phplem4on  7042  fidceq  7044  dif1en  7054  fin0  7060  fin0or  7061  isinfinf  7072  eqsndc  7081  infm  7082  en2eqpr  7085  fiuni  7161  supelti  7185  djudom  7276  difinfsn  7283  enomnilem  7321  enmkvlem  7344  enwomnilem  7352  exmidfodomrlemim  7395  exmidaclem  7406  cc2lem  7468  cc3  7470  genpml  7720  genpmu  7721  ltexprlemm  7803  ltexprlemfl  7812  ltexprlemfu  7814  suplocsr  8012  axpre-suploc  8105  eqord1  8646  nn1suc  9145  nninfdcex  10474  zsupssdc  10475  seq3f1oleml  10755  zfz1isolem1  11080  eulerth  12776  4sqlem14  12948  4sqlem17  12951  4sqlem18  12952  ennnfonelemim  13016  exmidunben  13018  enctlem  13024  ctiunct  13032  unct  13034  omctfn  13035  omiunct  13036  relelbasov  13116  issubg2m  13747  lmff  14944  txcn  14970  suplociccreex  15319  suplociccex  15320  wlkvtxiedg  16117  wlkvtxiedgg  16118  wlkreslem  16148  1dom1el  16463  3dom  16465  subctctexmid  16479  exmidsbthrlem  16504  sbthom  16508