Theorem exlimdv 1868

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

Syntax hints:   -> wi 4   E.wex 1541

This theorem was proved from axioms:  ax-mp 5  ax-1 6  ax-2 7  ax-ia1 106  ax-5 1496  ax-gen 1498  ax-ie2 1543  ax-17 1575

This theorem depends on definitions:  df-bi 117

This theorem is referenced by:  ax11v2  1869  exlimdvv  1949  exlimddv  1950  tpid3g  3812  sssnm  3863  pwntru  4317  euotd  4376  ralxfr2d  4590  rexxfr2d  4591  reldmm  4980  releldmb  4999  relelrnb  5000  elres  5079  iss  5089  imain  5443  elunirn  5945  ovmpt4g  6184  oprssdmm  6378  op1steq  6386  fo2ndf  6436  reldmtpos  6497  rntpos  6501  tfrlemibacc  6570  tfrlemibxssdm  6571  tfrlemibfn  6572  tfrexlem  6578  tfr1onlembacc  6586  tfr1onlembxssdm  6587  tfr1onlembfn  6588  tfrcllembacc  6599  tfrcllembxssdm  6600  tfrcllembfn  6601  map0g  6935  dom1o  7082  xpdom3m  7098  phplem4  7122  phpm  7133  findcard2  7159  findcard2s  7160  ac6sfi  7168  fiintim  7204  xpfi  7205  fidcenum  7239  ordiso  7340  ctmlemr  7412  ctm  7413  ctssdc  7417  pm54.43  7500  exmidfodomrlemim  7517  iftrueb01  7546  pw1m  7547  recclnq  7723  ltexnqq  7739  ltbtwnnqq  7746  recexprlemss1l  7966  recexprlemss1u  7967  negm  9965  ioom  10644  seq3f1olemp  10901  fiinfnf1o  11174  fihashf1rn  11176  climcau  12057  summodclem2  12093  zsumdc  12095  isumz  12100  fsumf1o  12101  fisumss  12103  fsumcl2lem  12109  fsumadd  12117  fsummulc2  12159  ntrivcvgap  12259  prodmodclem2  12288  zproddc  12290  prod1dc  12297  fprodf1o  12299  fprodssdc  12301  fprodmul  12302  nnmindc  12755  uzwodc  12758  pceu  13018  4sqlemafi  13118  4sqlem12  13125  ennnfone  13260  enctlem  13267  unct  13277  gsumfzval  13654  sgrpidmndm  13681  gfsumval  14102  subrngintm  14458  subrgintm  14489  islssm  14631  lss0cl  14643  islidlm  14753  eltg3  15048  tgtop  15059  tgidm  15065  tgrest  15160  tgcn  15199  xblm  15408  dvfgg  15679  dvcnp2cntop  15690  2lgslem1  16090  pwtrufal  16897