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  3754  pwntru  4199  euotd  4254  ralxfr2d  4464  rexxfr2d  4465  releldmb  4864  relelrnb  4865  elres  4943  iss  4953  imain  5298  elunirn  5766  ovmpt4g  5996  oprssdmm  6171  op1steq  6179  fo2ndf  6227  reldmtpos  6253  rntpos  6257  tfrlemibacc  6326  tfrlemibxssdm  6327  tfrlemibfn  6328  tfrexlem  6334  tfr1onlembacc  6342  tfr1onlembxssdm  6343  tfr1onlembfn  6344  tfrcllembacc  6355  tfrcllembxssdm  6356  tfrcllembfn  6357  map0g  6687  xpdom3m  6833  phplem4  6854  phpm  6864  findcard2  6888  findcard2s  6889  ac6sfi  6897  fiintim  6927  xpfi  6928  fidcenum  6954  ordiso  7034  ctmlemr  7106  ctm  7107  ctssdc  7111  pm54.43  7188  exmidfodomrlemim  7199  recclnq  7390  ltexnqq  7406  ltbtwnnqq  7413  recexprlemss1l  7633  recexprlemss1u  7634  negm  9613  ioom  10258  seq3f1olemp  10499  fiinfnf1o  10761  fihashf1rn  10763  climcau  11350  summodclem2  11385  zsumdc  11387  isumz  11392  fsumf1o  11393  fisumss  11395  fsumcl2lem  11401  fsumadd  11409  fsummulc2  11451  ntrivcvgap  11551  prodmodclem2  11580  zproddc  11582  prod1dc  11589  fprodf1o  11591  fprodssdc  11593  fprodmul  11594  nnmindc  12029  uzwodc  12032  pceu  12289  ennnfone  12420  enctlem  12427  unct  12437  sgrpidmndm  12775  subrgintm  13324  eltg3  13450  tgtop  13461  tgidm  13467  tgrest  13562  tgcn  13601  xblm  13810  dvfgg  14050  dvcnp2cntop  14056  pwtrufal  14629