Theorem exlimddv 1954

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

This proof depends on syntax axioms:   -> wi 4   /\ wa 104   E.wex 1545

This proof depends on axioms:  ax-mp 5  ax-1 6  ax-2 7  ax-ia1 106  ax-ia3 108  ax-5 1500  ax-gen 1502  ax-ie2 1547  ax-17 1579

This proof depends on definitions:  df-bi 117

This theorem is used by:  fvmptdv2  5798  tfrlemi14d  6608  tfrexlem  6609  tfr1onlemres  6624  tfrcllemres  6637  tfrcldm  6638  erref  6831  1dom1el  7111  en2  7116  en2m  7117  xpdom2  7133  dom0  7142  xpen  7149  mapdom1g  7151  phplem4dom  7167  phplem4on  7173  fidceq  7175  dif1en  7187  fin0  7193  fin0or  7194  isinfinf  7205  eqsndc  7214  infm  7215  en2eqpr  7218  fiuni  7317  supelti  7348  djudom  7439  difinfsn  7446  enomnilem  7484  enmkvlem  7507  enwomnilem  7515  exmidfodomrlemim  7559  exmidaclem  7570  cc2lem  7638  cc3  7640  genpml  7890  genpmu  7891  ltexprlemm  7973  ltexprlemfl  7982  ltexprlemfu  7984  suplocsr  8182  axpre-suploc  8275  eqord1  8818  nn1suc  9332  nninfdcex  10689  zsupssdc  10690  seq3f1oleml  10974  zfz1isolem1  11314  eulerth  13040  4sqlem14  13212  4sqlem17  13215  4sqlem18  13216  ennnfonelemim  13373  exmidunben  13375  enctlem  13381  ctiunct  13389  unct  13391  omctfn  13392  omiunct  13393  relelbasov  13474  issubg2m  14051  gsump1  14247  gsumf1ofi  14250  gsummhmfi  14264  gsumressfi  14267  opprringb  14495  lmff  15475  txcn  15501  suplociccreex  15850  suplociccex  15851  wlkvtxiedg  16791  wlkvtxiedgg  16792  wlkreslem  16824  eulerpathum  16927  3dom  17223  subctctexmid  17235  exmidsbthrlem  17273  sbthom  17277