Theorem exlimdv 1799

Description: Deduction from Theorem 19.23 of [Margaris] p. 90. (Contributed by NM, 27-Apr-1994.)

Hypothesis

Ref	Expression
exlimdv.1	|- ( ph -> ( ps -> ch ) )

Assertion

Ref	Expression
exlimdv	|- ( ph -> ( E. x ps -> ch ) )

Distinct variable groups:   ch, x   ph, x

Allowed substitution hint:   ps( x)

Proof of Theorem exlimdv

Step	Hyp	Ref	Expression
1		ax-17 1506	. 2 |- ( ph -> A. x ph )
2		ax-17 1506	. 2 |- ( ch -> A. x ch )
3		exlimdv.1	. 2 |- ( ph -> ( ps -> ch ) )
4	1, 2, 3	exlimdh 1576	1 |- ( ph -> ( E. x ps -> ch ) )

Syntax hints:   -> wi 4   E.wex 1472

This theorem was proved from axioms:  ax-mp 5  ax-1 6  ax-2 7  ax-ia1 105  ax-5 1427  ax-gen 1429  ax-ie2 1474  ax-17 1506

This theorem depends on definitions:  df-bi 116

This theorem is referenced by:  ax11v2  1800  exlimdvv  1877  exlimddv  1878  tpid3g  3674  sssnm  3717  pwntru  4160  euotd  4214  ralxfr2d  4423  rexxfr2d  4424  releldmb  4822  relelrnb  4823  elres  4901  iss  4911  imain  5251  elunirn  5713  ovmpt4g  5940  oprssdmm  6116  op1steq  6124  fo2ndf  6171  reldmtpos  6197  rntpos  6201  tfrlemibacc  6270  tfrlemibxssdm  6271  tfrlemibfn  6272  tfrexlem  6278  tfr1onlembacc  6286  tfr1onlembxssdm  6287  tfr1onlembfn  6288  tfrcllembacc  6299  tfrcllembxssdm  6300  tfrcllembfn  6301  map0g  6630  xpdom3m  6776  phplem4  6797  phpm  6807  findcard2  6831  findcard2s  6832  ac6sfi  6840  fiintim  6870  xpfi  6871  fidcenum  6897  ordiso  6974  ctmlemr  7046  ctm  7047  ctssdc  7051  pm54.43  7119  exmidfodomrlemim  7130  recclnq  7306  ltexnqq  7322  ltbtwnnqq  7329  recexprlemss1l  7549  recexprlemss1u  7550  negm  9517  ioom  10153  seq3f1olemp  10394  fiinfnf1o  10653  fihashf1rn  10656  climcau  11237  summodclem2  11272  zsumdc  11274  isumz  11279  fsumf1o  11280  fisumss  11282  fsumcl2lem  11288  fsumadd  11296  fsummulc2  11338  ntrivcvgap  11438  prodmodclem2  11467  zproddc  11469  prod1dc  11476  fprodf1o  11478  fprodssdc  11480  fprodmul  11481  ennnfone  12137  enctlem  12144  unct  12154  eltg3  12428  tgtop  12439  tgidm  12445  tgrest  12540  tgcn  12579  xblm  12788  dvfgg  13028  dvcnp2cntop  13034  pwtrufal  13540