Theorem exlimddv 1913

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

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

This theorem was proved from axioms:  ax-mp 5  ax-1 6  ax-2 7  ax-ia1 106  ax-ia3 108  ax-5 1461  ax-gen 1463  ax-ie2 1508  ax-17 1540

This theorem depends on definitions:  df-bi 117

This theorem is referenced by:  fvmptdv2  5651  tfrlemi14d  6391  tfrexlem  6392  tfr1onlemres  6407  tfrcllemres  6420  tfrcldm  6421  erref  6612  xpdom2  6890  dom0  6899  xpen  6906  mapdom1g  6908  phplem4dom  6923  phplem4on  6928  fidceq  6930  dif1en  6940  fin0  6946  fin0or  6947  isinfinf  6958  infm  6965  en2eqpr  6968  fiuni  7044  supelti  7068  djudom  7159  difinfsn  7166  enomnilem  7204  enmkvlem  7227  enwomnilem  7235  exmidfodomrlemim  7268  exmidaclem  7275  cc2lem  7333  cc3  7335  genpml  7584  genpmu  7585  ltexprlemm  7667  ltexprlemfl  7676  ltexprlemfu  7678  suplocsr  7876  axpre-suploc  7969  eqord1  8510  nn1suc  9009  nninfdcex  10327  zsupssdc  10328  seq3f1oleml  10608  zfz1isolem1  10932  eulerth  12401  4sqlem14  12573  4sqlem17  12576  4sqlem18  12577  ennnfonelemim  12641  exmidunben  12643  enctlem  12649  ctiunct  12657  unct  12659  omctfn  12660  omiunct  12661  relelbasov  12740  issubg2m  13319  lmff  14485  txcn  14511  suplociccreex  14860  suplociccex  14861  1dom1el  15637  subctctexmid  15645  exmidsbthrlem  15666  sbthom  15670