Theorem exlimdv 1842

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

Syntax hints:   -> wi 4   E.wex 1515

This theorem was proved from axioms:  ax-mp 5  ax-1 6  ax-2 7  ax-ia1 106  ax-5 1470  ax-gen 1472  ax-ie2 1517  ax-17 1549

This theorem depends on definitions:  df-bi 117

This theorem is referenced by:  ax11v2  1843  exlimdvv  1921  exlimddv  1922  tpid3g  3748  sssnm  3795  pwntru  4244  euotd  4300  ralxfr2d  4512  rexxfr2d  4513  releldmb  4916  relelrnb  4917  elres  4996  iss  5006  imain  5357  elunirn  5837  ovmpt4g  6070  oprssdmm  6259  op1steq  6267  fo2ndf  6315  reldmtpos  6341  rntpos  6345  tfrlemibacc  6414  tfrlemibxssdm  6415  tfrlemibfn  6416  tfrexlem  6422  tfr1onlembacc  6430  tfr1onlembxssdm  6431  tfr1onlembfn  6432  tfrcllembacc  6443  tfrcllembxssdm  6444  tfrcllembfn  6445  map0g  6777  xpdom3m  6931  phplem4  6954  phpm  6964  findcard2  6988  findcard2s  6989  ac6sfi  6997  fiintim  7030  xpfi  7031  fidcenum  7060  ordiso  7140  ctmlemr  7212  ctm  7213  ctssdc  7217  pm54.43  7300  exmidfodomrlemim  7311  recclnq  7507  ltexnqq  7523  ltbtwnnqq  7530  recexprlemss1l  7750  recexprlemss1u  7751  negm  9738  ioom  10405  seq3f1olemp  10662  fiinfnf1o  10933  fihashf1rn  10935  climcau  11691  summodclem2  11726  zsumdc  11728  isumz  11733  fsumf1o  11734  fisumss  11736  fsumcl2lem  11742  fsumadd  11750  fsummulc2  11792  ntrivcvgap  11892  prodmodclem2  11921  zproddc  11923  prod1dc  11930  fprodf1o  11932  fprodssdc  11934  fprodmul  11935  nnmindc  12388  uzwodc  12391  pceu  12651  4sqlemafi  12751  4sqlem12  12758  ennnfone  12829  enctlem  12836  unct  12846  gsumfzval  13256  sgrpidmndm  13285  subrngintm  14007  subrgintm  14038  islssm  14152  lss0cl  14164  islidlm  14274  eltg3  14562  tgtop  14573  tgidm  14579  tgrest  14674  tgcn  14713  xblm  14922  dvfgg  15193  dvcnp2cntop  15204  2lgslem1  15601  pwtrufal  15971