Theorem exlimddv 1833

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

Syntax hints:   → wi 4   ∧ wa 103  ∃wex 1433

This theorem was proved from axioms:  ax-1 5  ax-2 6  ax-mp 7  ax-ia1 105  ax-ia3 107  ax-5 1388  ax-gen 1390  ax-ie2 1435  ax-17 1471

This theorem depends on definitions:  df-bi 116

This theorem is referenced by:  fvmptdv2  5428  tfrlemi14d  6136  tfrexlem  6137  tfr1onlemres  6152  tfrcllemres  6165  tfrcldm  6166  erref  6352  xpdom2  6627  dom0  6634  xpen  6641  mapdom1g  6643  phplem4dom  6658  phplem4on  6663  fidceq  6665  dif1en  6675  fin0  6681  fin0or  6682  isinfinf  6693  infm  6700  en2eqpr  6703  supelti  6777  djudom  6863  enomnilem  6881  exmidfodomrlemim  6924  genpml  7173  genpmu  7174  ltexprlemm  7256  ltexprlemfl  7265  ltexprlemfu  7267  eqord1  8058  nn1suc  8539  seq3f1oleml  10053  zfz1isolem1  10360  lmff  12100  exmidsbthrlem  12617