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  5732  tfrlemi14d  6494  tfrexlem  6495  tfr1onlemres  6510  tfrcllemres  6523  tfrcldm  6524  erref  6717  1dom1el  6988  en2  6993  en2m  6994  xpdom2  7010  dom0  7019  xpen  7026  mapdom1g  7028  phplem4dom  7043  phplem4on  7049  fidceq  7051  dif1en  7063  fin0  7069  fin0or  7070  isinfinf  7081  eqsndc  7090  infm  7091  en2eqpr  7094  fiuni  7171  supelti  7195  djudom  7286  difinfsn  7293  enomnilem  7331  enmkvlem  7354  enwomnilem  7362  exmidfodomrlemim  7405  exmidaclem  7416  cc2lem  7478  cc3  7480  genpml  7730  genpmu  7731  ltexprlemm  7813  ltexprlemfl  7822  ltexprlemfu  7824  suplocsr  8022  axpre-suploc  8115  eqord1  8656  nn1suc  9155  nninfdcex  10490  zsupssdc  10491  seq3f1oleml  10771  zfz1isolem1  11097  eulerth  12798  4sqlem14  12970  4sqlem17  12973  4sqlem18  12974  ennnfonelemim  13038  exmidunben  13040  enctlem  13046  ctiunct  13054  unct  13056  omctfn  13057  omiunct  13058  relelbasov  13138  issubg2m  13769  lmff  14966  txcn  14992  suplociccreex  15341  suplociccex  15342  wlkvtxiedg  16156  wlkvtxiedgg  16157  wlkreslem  16187  3dom  16537  subctctexmid  16551  exmidsbthrlem  16576  sbthom  16580