Theorem exlimddv 1898

Description: Existential elimination rule of natural deduction. (Contributed by Mario Carneiro, 15-Jun-2016.)

Hypotheses

Ref	Expression
exlimddv.1	|- ( ph -> E. x ps )
exlimddv.2	|- ( ( ph /\ ps ) -> ch )

Assertion

Ref	Expression
exlimddv	|- ( ph -> ch )

Distinct variable groups:   ch, x   ph, x

Allowed substitution hint:   ps( x)

Proof of Theorem exlimddv

Step	Hyp	Ref	Expression
1		exlimddv.1	. 2 |- ( ph -> E. x ps )
2		exlimddv.2	. . . 4 |- ( ( ph /\ ps ) -> ch )
3	2	ex 115	. . 3 |- ( ph -> ( ps -> ch ) )
4	3	exlimdv 1819	. 2 |- ( ph -> ( E. x ps -> ch ) )
5	1, 4	mpd 13	1 |- ( ph -> ch )

Syntax hints:   -> wi 4   /\ wa 104   E.wex 1492

This theorem was proved from axioms:  ax-mp 5  ax-1 6  ax-2 7  ax-ia1 106  ax-ia3 108  ax-5 1447  ax-gen 1449  ax-ie2 1494  ax-17 1526

This theorem depends on definitions:  df-bi 117

This theorem is referenced by:  fvmptdv2  5606  tfrlemi14d  6334  tfrexlem  6335  tfr1onlemres  6350  tfrcllemres  6363  tfrcldm  6364  erref  6555  xpdom2  6831  dom0  6838  xpen  6845  mapdom1g  6847  phplem4dom  6862  phplem4on  6867  fidceq  6869  dif1en  6879  fin0  6885  fin0or  6886  isinfinf  6897  infm  6904  en2eqpr  6907  fiuni  6977  supelti  7001  djudom  7092  difinfsn  7099  enomnilem  7136  enmkvlem  7159  enwomnilem  7167  exmidfodomrlemim  7200  exmidaclem  7207  cc2lem  7265  cc3  7267  genpml  7516  genpmu  7517  ltexprlemm  7599  ltexprlemfl  7608  ltexprlemfu  7610  suplocsr  7808  axpre-suploc  7901  eqord1  8440  nn1suc  8938  seq3f1oleml  10503  zfz1isolem1  10820  nninfdcex  11954  zsupssdc  11955  eulerth  12233  ennnfonelemim  12425  exmidunben  12427  enctlem  12433  ctiunct  12441  unct  12443  omctfn  12444  omiunct  12445  issubg2m  13049  lmff  13752  txcn  13778  suplociccreex  14105  suplociccex  14106  subctctexmid  14753  exmidsbthrlem  14773  sbthom  14777