Theorem exlimddv 1945

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

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

This theorem was proved from axioms:  ax-mp 5  ax-1 6  ax-2 7  ax-ia1 106  ax-ia3 108  ax-5 1493  ax-gen 1495  ax-ie2 1540  ax-17 1572

This theorem depends on definitions:  df-bi 117

This theorem is referenced by:  fvmptdv2  5717  tfrlemi14d  6469  tfrexlem  6470  tfr1onlemres  6485  tfrcllemres  6498  tfrcldm  6499  erref  6690  en2  6963  en2m  6964  xpdom2  6978  dom0  6987  xpen  6994  mapdom1g  6996  phplem4dom  7011  phplem4on  7017  fidceq  7019  dif1en  7029  fin0  7035  fin0or  7036  isinfinf  7047  infm  7054  en2eqpr  7057  fiuni  7133  supelti  7157  djudom  7248  difinfsn  7255  enomnilem  7293  enmkvlem  7316  enwomnilem  7324  exmidfodomrlemim  7367  exmidaclem  7378  cc2lem  7440  cc3  7442  genpml  7692  genpmu  7693  ltexprlemm  7775  ltexprlemfl  7784  ltexprlemfu  7786  suplocsr  7984  axpre-suploc  8077  eqord1  8618  nn1suc  9117  nninfdcex  10444  zsupssdc  10445  seq3f1oleml  10725  zfz1isolem1  11049  eulerth  12741  4sqlem14  12913  4sqlem17  12916  4sqlem18  12917  ennnfonelemim  12981  exmidunben  12983  enctlem  12989  ctiunct  12997  unct  12999  omctfn  13000  omiunct  13001  relelbasov  13081  issubg2m  13712  lmff  14908  txcn  14934  suplociccreex  15283  suplociccex  15284  1dom1el  16284  subctctexmid  16297  exmidsbthrlem  16321  sbthom  16325