Theorem exlimdv 1812

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

Syntax hints:   -> wi 4   E.wex 1485

This theorem was proved from axioms:  ax-mp 5  ax-1 6  ax-2 7  ax-ia1 105  ax-5 1440  ax-gen 1442  ax-ie2 1487  ax-17 1519

This theorem depends on definitions:  df-bi 116

This theorem is referenced by:  ax11v2  1813  exlimdvv  1890  exlimddv  1891  tpid3g  3698  sssnm  3741  pwntru  4185  euotd  4239  ralxfr2d  4449  rexxfr2d  4450  releldmb  4848  relelrnb  4849  elres  4927  iss  4937  imain  5280  elunirn  5745  ovmpt4g  5975  oprssdmm  6150  op1steq  6158  fo2ndf  6206  reldmtpos  6232  rntpos  6236  tfrlemibacc  6305  tfrlemibxssdm  6306  tfrlemibfn  6307  tfrexlem  6313  tfr1onlembacc  6321  tfr1onlembxssdm  6322  tfr1onlembfn  6323  tfrcllembacc  6334  tfrcllembxssdm  6335  tfrcllembfn  6336  map0g  6666  xpdom3m  6812  phplem4  6833  phpm  6843  findcard2  6867  findcard2s  6868  ac6sfi  6876  fiintim  6906  xpfi  6907  fidcenum  6933  ordiso  7013  ctmlemr  7085  ctm  7086  ctssdc  7090  pm54.43  7167  exmidfodomrlemim  7178  recclnq  7354  ltexnqq  7370  ltbtwnnqq  7377  recexprlemss1l  7597  recexprlemss1u  7598  negm  9574  ioom  10217  seq3f1olemp  10458  fiinfnf1o  10720  fihashf1rn  10723  climcau  11310  summodclem2  11345  zsumdc  11347  isumz  11352  fsumf1o  11353  fisumss  11355  fsumcl2lem  11361  fsumadd  11369  fsummulc2  11411  ntrivcvgap  11511  prodmodclem2  11540  zproddc  11542  prod1dc  11549  fprodf1o  11551  fprodssdc  11553  fprodmul  11554  nnmindc  11989  uzwodc  11992  pceu  12249  ennnfone  12380  enctlem  12387  unct  12397  sgrpidmndm  12656  eltg3  12851  tgtop  12862  tgidm  12868  tgrest  12963  tgcn  13002  xblm  13211  dvfgg  13451  dvcnp2cntop  13457  pwtrufal  14030