Theorem exlimddv 1871

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

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

This theorem was proved from axioms:  ax-mp 5  ax-1 6  ax-2 7  ax-ia1 105  ax-ia3 107  ax-5 1424  ax-gen 1426  ax-ie2 1471  ax-17 1507

This theorem depends on definitions:  df-bi 116

This theorem is referenced by:  fvmptdv2  5518  tfrlemi14d  6238  tfrexlem  6239  tfr1onlemres  6254  tfrcllemres  6267  tfrcldm  6268  erref  6457  xpdom2  6733  dom0  6740  xpen  6747  mapdom1g  6749  phplem4dom  6764  phplem4on  6769  fidceq  6771  dif1en  6781  fin0  6787  fin0or  6788  isinfinf  6799  infm  6806  en2eqpr  6809  fiuni  6874  supelti  6897  djudom  6986  difinfsn  6993  enomnilem  7018  enmkvlem  7043  enwomnilem  7050  exmidfodomrlemim  7074  exmidaclem  7081  cc2lem  7098  cc3  7100  genpml  7349  genpmu  7350  ltexprlemm  7432  ltexprlemfl  7441  ltexprlemfu  7443  suplocsr  7641  axpre-suploc  7734  eqord1  8269  nn1suc  8763  seq3f1oleml  10307  zfz1isolem1  10615  ennnfonelemim  11973  exmidunben  11975  enctlem  11981  ctiunct  11989  unct  11991  omctfn  11992  omiunct  11993  lmff  12457  txcn  12483  suplociccreex  12810  suplociccex  12811  subctctexmid  13369  exmidsbthrlem  13392  sbthom  13396