Theorem exlimdv 1807

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

Syntax hints:   -> wi 4   E.wex 1480

This theorem was proved from axioms:  ax-mp 5  ax-1 6  ax-2 7  ax-ia1 105  ax-5 1435  ax-gen 1437  ax-ie2 1482  ax-17 1514

This theorem depends on definitions:  df-bi 116

This theorem is referenced by:  ax11v2  1808  exlimdvv  1885  exlimddv  1886  tpid3g  3690  sssnm  3733  pwntru  4177  euotd  4231  ralxfr2d  4441  rexxfr2d  4442  releldmb  4840  relelrnb  4841  elres  4919  iss  4929  imain  5269  elunirn  5733  ovmpt4g  5960  oprssdmm  6136  op1steq  6144  fo2ndf  6191  reldmtpos  6217  rntpos  6221  tfrlemibacc  6290  tfrlemibxssdm  6291  tfrlemibfn  6292  tfrexlem  6298  tfr1onlembacc  6306  tfr1onlembxssdm  6307  tfr1onlembfn  6308  tfrcllembacc  6319  tfrcllembxssdm  6320  tfrcllembfn  6321  map0g  6650  xpdom3m  6796  phplem4  6817  phpm  6827  findcard2  6851  findcard2s  6852  ac6sfi  6860  fiintim  6890  xpfi  6891  fidcenum  6917  ordiso  6997  ctmlemr  7069  ctm  7070  ctssdc  7074  pm54.43  7142  exmidfodomrlemim  7153  recclnq  7329  ltexnqq  7345  ltbtwnnqq  7352  recexprlemss1l  7572  recexprlemss1u  7573  negm  9549  ioom  10192  seq3f1olemp  10433  fiinfnf1o  10695  fihashf1rn  10698  climcau  11284  summodclem2  11319  zsumdc  11321  isumz  11326  fsumf1o  11327  fisumss  11329  fsumcl2lem  11335  fsumadd  11343  fsummulc2  11385  ntrivcvgap  11485  prodmodclem2  11514  zproddc  11516  prod1dc  11523  fprodf1o  11525  fprodssdc  11527  fprodmul  11528  nnmindc  11963  uzwodc  11966  pceu  12223  ennnfone  12354  enctlem  12361  unct  12371  eltg3  12657  tgtop  12668  tgidm  12674  tgrest  12769  tgcn  12808  xblm  13017  dvfgg  13257  dvcnp2cntop  13263  pwtrufal  13837