Theorem exlimdv 1792

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 1507	. 2 |- ( ph -> A. x ph )
2		ax-17 1507	. 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 1469

This theorem was proved from axioms:  ax-mp 5  ax-1 6  ax-2 7  ax-ia1 105  ax-5 1424  ax-gen 1426  ax-ie2 1471  ax-17 1507

This theorem depends on definitions:  df-bi 116

This theorem is referenced by:  ax11v2  1793  exlimdvv  1870  exlimddv  1871  tpid3g  3646  sssnm  3689  pwntru  4130  euotd  4184  ralxfr2d  4393  rexxfr2d  4394  releldmb  4784  relelrnb  4785  elres  4863  iss  4873  imain  5213  elunirn  5675  ovmpt4g  5901  oprssdmm  6077  op1steq  6085  fo2ndf  6132  reldmtpos  6158  rntpos  6162  tfrlemibacc  6231  tfrlemibxssdm  6232  tfrlemibfn  6233  tfrexlem  6239  tfr1onlembacc  6247  tfr1onlembxssdm  6248  tfr1onlembfn  6249  tfrcllembacc  6260  tfrcllembxssdm  6261  tfrcllembfn  6262  map0g  6590  xpdom3m  6736  phplem4  6757  phpm  6767  findcard2  6791  findcard2s  6792  ac6sfi  6800  fiintim  6825  xpfi  6826  fidcenum  6852  ordiso  6929  ctmlemr  7001  ctm  7002  ctssdc  7006  pm54.43  7063  exmidfodomrlemim  7074  recclnq  7224  ltexnqq  7240  ltbtwnnqq  7247  recexprlemss1l  7467  recexprlemss1u  7468  negm  9434  ioom  10069  seq3f1olemp  10306  fiinfnf1o  10564  fihashf1rn  10567  climcau  11148  summodclem2  11183  zsumdc  11185  isumz  11190  fsumf1o  11191  fisumss  11193  fsumcl2lem  11199  fsumadd  11207  fsummulc2  11249  ntrivcvgap  11349  prodmodclem2  11378  zproddc  11380  ennnfone  11974  enctlem  11981  unct  11991  eltg3  12265  tgtop  12276  tgidm  12282  tgrest  12377  tgcn  12416  xblm  12625  dvfgg  12865  dvcnp2cntop  12871  pwtrufal  13365