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  3709  sssnm  3756  pwntru  4201  euotd  4256  ralxfr2d  4466  rexxfr2d  4467  releldmb  4866  relelrnb  4867  elres  4945  iss  4955  imain  5300  elunirn  5769  ovmpt4g  5999  oprssdmm  6174  op1steq  6182  fo2ndf  6230  reldmtpos  6256  rntpos  6260  tfrlemibacc  6329  tfrlemibxssdm  6330  tfrlemibfn  6331  tfrexlem  6337  tfr1onlembacc  6345  tfr1onlembxssdm  6346  tfr1onlembfn  6347  tfrcllembacc  6358  tfrcllembxssdm  6359  tfrcllembfn  6360  map0g  6690  xpdom3m  6836  phplem4  6857  phpm  6867  findcard2  6891  findcard2s  6892  ac6sfi  6900  fiintim  6930  xpfi  6931  fidcenum  6957  ordiso  7037  ctmlemr  7109  ctm  7110  ctssdc  7114  pm54.43  7191  exmidfodomrlemim  7202  recclnq  7393  ltexnqq  7409  ltbtwnnqq  7416  recexprlemss1l  7636  recexprlemss1u  7637  negm  9617  ioom  10263  seq3f1olemp  10504  fiinfnf1o  10768  fihashf1rn  10770  climcau  11357  summodclem2  11392  zsumdc  11394  isumz  11399  fsumf1o  11400  fisumss  11402  fsumcl2lem  11408  fsumadd  11416  fsummulc2  11458  ntrivcvgap  11558  prodmodclem2  11587  zproddc  11589  prod1dc  11596  fprodf1o  11598  fprodssdc  11600  fprodmul  11601  nnmindc  12037  uzwodc  12040  pceu  12297  ennnfone  12428  enctlem  12435  unct  12445  sgrpidmndm  12826  subrgintm  13369  lss0cl  13460  eltg3  13596  tgtop  13607  tgidm  13613  tgrest  13708  tgcn  13747  xblm  13956  dvfgg  14196  dvcnp2cntop  14202  pwtrufal  14786