Theorem exlimddv 1870

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

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

This theorem was proved from axioms:  ax-mp 5  ax-1 6  ax-2 7  ax-ia1 105  ax-ia3 107  ax-5 1423  ax-gen 1425  ax-ie2 1470  ax-17 1506

This theorem depends on definitions:  df-bi 116

This theorem is referenced by:  fvmptdv2  5510  tfrlemi14d  6230  tfrexlem  6231  tfr1onlemres  6246  tfrcllemres  6259  tfrcldm  6260  erref  6449  xpdom2  6725  dom0  6732  xpen  6739  mapdom1g  6741  phplem4dom  6756  phplem4on  6761  fidceq  6763  dif1en  6773  fin0  6779  fin0or  6780  isinfinf  6791  infm  6798  en2eqpr  6801  fiuni  6866  supelti  6889  djudom  6978  difinfsn  6985  enomnilem  7010  exmidfodomrlemim  7057  exmidaclem  7064  genpml  7325  genpmu  7326  ltexprlemm  7408  ltexprlemfl  7417  ltexprlemfu  7419  suplocsr  7617  axpre-suploc  7710  eqord1  8245  nn1suc  8739  seq3f1oleml  10276  zfz1isolem1  10583  ennnfonelemim  11937  exmidunben  11939  enctlem  11945  ctiunct  11953  unct  11954  lmff  12418  txcn  12444  suplociccreex  12771  suplociccex  12772  subctctexmid  13196  exmidsbthrlem  13217  sbthom  13221