Theorem exlimdv 1819

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

Syntax hints:   -> wi 4   E.wex 1492

This theorem was proved from axioms:  ax-mp 5  ax-1 6  ax-2 7  ax-ia1 106  ax-5 1447  ax-gen 1449  ax-ie2 1494  ax-17 1526

This theorem depends on definitions:  df-bi 117

This theorem is referenced by:  ax11v2  1820  exlimdvv  1897  exlimddv  1898  tpid3g  3707  sssnm  3753  pwntru  4197  euotd  4252  ralxfr2d  4462  rexxfr2d  4463  releldmb  4861  relelrnb  4862  elres  4940  iss  4950  imain  5295  elunirn  5762  ovmpt4g  5992  oprssdmm  6167  op1steq  6175  fo2ndf  6223  reldmtpos  6249  rntpos  6253  tfrlemibacc  6322  tfrlemibxssdm  6323  tfrlemibfn  6324  tfrexlem  6330  tfr1onlembacc  6338  tfr1onlembxssdm  6339  tfr1onlembfn  6340  tfrcllembacc  6351  tfrcllembxssdm  6352  tfrcllembfn  6353  map0g  6683  xpdom3m  6829  phplem4  6850  phpm  6860  findcard2  6884  findcard2s  6885  ac6sfi  6893  fiintim  6923  xpfi  6924  fidcenum  6950  ordiso  7030  ctmlemr  7102  ctm  7103  ctssdc  7107  pm54.43  7184  exmidfodomrlemim  7195  recclnq  7386  ltexnqq  7402  ltbtwnnqq  7409  recexprlemss1l  7629  recexprlemss1u  7630  negm  9609  ioom  10254  seq3f1olemp  10495  fiinfnf1o  10757  fihashf1rn  10759  climcau  11346  summodclem2  11381  zsumdc  11383  isumz  11388  fsumf1o  11389  fisumss  11391  fsumcl2lem  11397  fsumadd  11405  fsummulc2  11447  ntrivcvgap  11547  prodmodclem2  11576  zproddc  11578  prod1dc  11585  fprodf1o  11587  fprodssdc  11589  fprodmul  11590  nnmindc  12025  uzwodc  12028  pceu  12285  ennnfone  12416  enctlem  12423  unct  12433  sgrpidmndm  12751  eltg3  13339  tgtop  13350  tgidm  13356  tgrest  13451  tgcn  13490  xblm  13699  dvfgg  13939  dvcnp2cntop  13945  pwtrufal  14518