Theorem exlimddv 1947

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 1867	. 2 ⊢ (𝜑 → (∃𝑥𝜓 → 𝜒))
5	1, 4	mpd 13	1 ⊢ (𝜑 → 𝜒)

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

This theorem was proved from axioms:  ax-mp 5  ax-1 6  ax-2 7  ax-ia1 106  ax-ia3 108  ax-5 1495  ax-gen 1497  ax-ie2 1542  ax-17 1574

This theorem depends on definitions:  df-bi 117

This theorem is referenced by:  fvmptdv2  5736  tfrlemi14d  6499  tfrexlem  6500  tfr1onlemres  6515  tfrcllemres  6528  tfrcldm  6529  erref  6722  1dom1el  6993  en2  6998  en2m  6999  xpdom2  7015  dom0  7024  xpen  7031  mapdom1g  7033  phplem4dom  7048  phplem4on  7054  fidceq  7056  dif1en  7068  fin0  7074  fin0or  7075  isinfinf  7086  eqsndc  7095  infm  7096  en2eqpr  7099  fiuni  7177  supelti  7201  djudom  7292  difinfsn  7299  enomnilem  7337  enmkvlem  7360  enwomnilem  7368  exmidfodomrlemim  7412  exmidaclem  7423  cc2lem  7485  cc3  7487  genpml  7737  genpmu  7738  ltexprlemm  7820  ltexprlemfl  7829  ltexprlemfu  7831  suplocsr  8029  axpre-suploc  8122  eqord1  8663  nn1suc  9162  nninfdcex  10498  zsupssdc  10499  seq3f1oleml  10779  zfz1isolem1  11105  eulerth  12810  4sqlem14  12982  4sqlem17  12985  4sqlem18  12986  ennnfonelemim  13050  exmidunben  13052  enctlem  13058  ctiunct  13066  unct  13068  omctfn  13069  omiunct  13070  relelbasov  13150  issubg2m  13781  lmff  14979  txcn  15005  suplociccreex  15354  suplociccex  15355  wlkvtxiedg  16202  wlkvtxiedgg  16203  wlkreslem  16235  eulerpathum  16338  3dom  16613  subctctexmid  16627  exmidsbthrlem  16652  sbthom  16656  gfsump1  16712