Theorem exlimddv 1922

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 1842	. 2 |- ( ph -> ( E. x ps -> ch ) )
5	1, 4	mpd 13	1 |- ( ph -> ch )

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

This theorem was proved from axioms:  ax-mp 5  ax-1 6  ax-2 7  ax-ia1 106  ax-ia3 108  ax-5 1470  ax-gen 1472  ax-ie2 1517  ax-17 1549

This theorem depends on definitions:  df-bi 117

This theorem is referenced by:  fvmptdv2  5671  tfrlemi14d  6421  tfrexlem  6422  tfr1onlemres  6437  tfrcllemres  6450  tfrcldm  6451  erref  6642  en2  6914  xpdom2  6928  dom0  6937  xpen  6944  mapdom1g  6946  phplem4dom  6961  phplem4on  6966  fidceq  6968  dif1en  6978  fin0  6984  fin0or  6985  isinfinf  6996  infm  7003  en2eqpr  7006  fiuni  7082  supelti  7106  djudom  7197  difinfsn  7204  enomnilem  7242  enmkvlem  7265  enwomnilem  7273  exmidfodomrlemim  7311  exmidaclem  7322  cc2lem  7380  cc3  7382  genpml  7632  genpmu  7633  ltexprlemm  7715  ltexprlemfl  7724  ltexprlemfu  7726  suplocsr  7924  axpre-suploc  8017  eqord1  8558  nn1suc  9057  nninfdcex  10382  zsupssdc  10383  seq3f1oleml  10663  zfz1isolem1  10987  eulerth  12588  4sqlem14  12760  4sqlem17  12763  4sqlem18  12764  ennnfonelemim  12828  exmidunben  12830  enctlem  12836  ctiunct  12844  unct  12846  omctfn  12847  omiunct  12848  relelbasov  12927  issubg2m  13558  lmff  14754  txcn  14780  suplociccreex  15129  suplociccex  15130  1dom1el  15964  subctctexmid  15974  exmidsbthrlem  15998  sbthom  16002