Theorem exlimddv 1910

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

Syntax hints:   → wi 4   ∧ wa 104  ∃wex 1503

This theorem was proved from axioms:  ax-mp 5  ax-1 6  ax-2 7  ax-ia1 106  ax-ia3 108  ax-5 1458  ax-gen 1460  ax-ie2 1505  ax-17 1537

This theorem depends on definitions:  df-bi 117

This theorem is referenced by:  fvmptdv2  5647  tfrlemi14d  6386  tfrexlem  6387  tfr1onlemres  6402  tfrcllemres  6415  tfrcldm  6416  erref  6607  xpdom2  6885  dom0  6894  xpen  6901  mapdom1g  6903  phplem4dom  6918  phplem4on  6923  fidceq  6925  dif1en  6935  fin0  6941  fin0or  6942  isinfinf  6953  infm  6960  en2eqpr  6963  fiuni  7037  supelti  7061  djudom  7152  difinfsn  7159  enomnilem  7197  enmkvlem  7220  enwomnilem  7228  exmidfodomrlemim  7261  exmidaclem  7268  cc2lem  7326  cc3  7328  genpml  7577  genpmu  7578  ltexprlemm  7660  ltexprlemfl  7669  ltexprlemfu  7671  suplocsr  7869  axpre-suploc  7962  eqord1  8502  nn1suc  9001  seq3f1oleml  10587  zfz1isolem1  10911  nninfdcex  12090  zsupssdc  12091  eulerth  12371  4sqlem14  12542  4sqlem17  12545  4sqlem18  12546  ennnfonelemim  12581  exmidunben  12583  enctlem  12589  ctiunct  12597  unct  12599  omctfn  12600  omiunct  12601  relelbasov  12680  issubg2m  13259  lmff  14417  txcn  14443  suplociccreex  14778  suplociccex  14779  1dom1el  15483  subctctexmid  15491  exmidsbthrlem  15512  sbthom  15516