Theorem exlimddv 1819

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

Syntax hints:   → wi 4   ∧ wa 102  ∃wex 1421

This theorem was proved from axioms:  ax-1 5  ax-2 6  ax-mp 7  ax-ia1 104  ax-ia3 106  ax-5 1376  ax-gen 1378  ax-ie2 1423  ax-17 1459

This theorem depends on definitions:  df-bi 115

This theorem is referenced by:  fvmptdv2  5281  tfrlemi14d  5970  tfrexlem  5971  erref  6149  xpdom2  6328  phplem4dom  6348  phplem4on  6353  fidceq  6354  dif1en  6364  fin0  6369  fin0or  6370  en2eqpr  6380  supelti  6415  genpml  6707  genpmu  6708  ltexprlemm  6790  ltexprlemfl  6799  ltexprlemfu  6801  nn1suc  8058