Theorem exlimdv 1865

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 1572	. 2 |- ( ph -> A. x ph )
2		ax-17 1572	. 2 |- ( ch -> A. x ch )
3		exlimdv.1	. 2 |- ( ph -> ( ps -> ch ) )
4	1, 2, 3	exlimdh 1642	1 |- ( ph -> ( E. x ps -> ch ) )

Syntax hints:   -> wi 4   E.wex 1538

This theorem was proved from axioms:  ax-mp 5  ax-1 6  ax-2 7  ax-ia1 106  ax-5 1493  ax-gen 1495  ax-ie2 1540  ax-17 1572

This theorem depends on definitions:  df-bi 117

This theorem is referenced by:  ax11v2  1866  exlimdvv  1944  exlimddv  1945  tpid3g  3782  sssnm  3832  pwntru  4283  euotd  4341  ralxfr2d  4555  rexxfr2d  4556  reldmm  4942  releldmb  4961  relelrnb  4962  elres  5041  iss  5051  imain  5403  elunirn  5896  ovmpt4g  6133  oprssdmm  6323  op1steq  6331  fo2ndf  6379  reldmtpos  6405  rntpos  6409  tfrlemibacc  6478  tfrlemibxssdm  6479  tfrlemibfn  6480  tfrexlem  6486  tfr1onlembacc  6494  tfr1onlembxssdm  6495  tfr1onlembfn  6496  tfrcllembacc  6507  tfrcllembxssdm  6508  tfrcllembfn  6509  map0g  6843  dom1o  6985  xpdom3m  7001  phplem4  7024  phpm  7035  findcard2  7059  findcard2s  7060  ac6sfi  7068  fiintim  7104  xpfi  7105  fidcenum  7134  ordiso  7214  ctmlemr  7286  ctm  7287  ctssdc  7291  pm54.43  7374  exmidfodomrlemim  7390  iftrueb01  7419  pw1m  7420  recclnq  7590  ltexnqq  7606  ltbtwnnqq  7613  recexprlemss1l  7833  recexprlemss1u  7834  negm  9822  ioom  10492  seq3f1olemp  10749  fiinfnf1o  11020  fihashf1rn  11022  climcau  11874  summodclem2  11909  zsumdc  11911  isumz  11916  fsumf1o  11917  fisumss  11919  fsumcl2lem  11925  fsumadd  11933  fsummulc2  11975  ntrivcvgap  12075  prodmodclem2  12104  zproddc  12106  prod1dc  12113  fprodf1o  12115  fprodssdc  12117  fprodmul  12118  nnmindc  12571  uzwodc  12574  pceu  12834  4sqlemafi  12934  4sqlem12  12941  ennnfone  13012  enctlem  13019  unct  13029  gsumfzval  13440  sgrpidmndm  13469  subrngintm  14192  subrgintm  14223  islssm  14337  lss0cl  14349  islidlm  14459  eltg3  14747  tgtop  14758  tgidm  14764  tgrest  14859  tgcn  14898  xblm  15107  dvfgg  15378  dvcnp2cntop  15389  2lgslem1  15786  pwtrufal  16450