Theorem exlimddv 1778

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

Syntax hints:   → wi 4   ∧ wa 97  ∃wex 1381

This theorem was proved from axioms:  ax-1 5  ax-2 6  ax-mp 7  ax-ia1 99  ax-ia3 101  ax-5 1336  ax-gen 1338  ax-ie2 1383  ax-17 1419

This theorem depends on definitions:  df-bi 110

This theorem is referenced by:  fvmptdv2  5260  tfrlemi14d  5947  tfrexlem  5948  erref  6126  xpdom2  6305  phplem4dom  6324  phplem4on  6329  fidceq  6330  dif1en  6337  fin0  6342  fin0or  6343  genpml  6615  genpmu  6616  ltexprlemm  6698  ltexprlemfl  6707  ltexprlemfu  6709  nn1suc  7933