Theorem exlimdv 1867

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

Syntax hints:   -> wi 4   E.wex 1540

This theorem was proved from axioms:  ax-mp 5  ax-1 6  ax-2 7  ax-ia1 106  ax-5 1495  ax-gen 1497  ax-ie2 1542  ax-17 1574

This theorem depends on definitions:  df-bi 117

This theorem is referenced by:  ax11v2  1868  exlimdvv  1946  exlimddv  1947  tpid3g  3787  sssnm  3837  pwntru  4289  euotd  4347  ralxfr2d  4561  rexxfr2d  4562  reldmm  4950  releldmb  4969  relelrnb  4970  elres  5049  iss  5059  imain  5412  elunirn  5907  ovmpt4g  6144  oprssdmm  6334  op1steq  6342  fo2ndf  6392  reldmtpos  6419  rntpos  6423  tfrlemibacc  6492  tfrlemibxssdm  6493  tfrlemibfn  6494  tfrexlem  6500  tfr1onlembacc  6508  tfr1onlembxssdm  6509  tfr1onlembfn  6510  tfrcllembacc  6521  tfrcllembxssdm  6522  tfrcllembfn  6523  map0g  6857  dom1o  7002  xpdom3m  7018  phplem4  7041  phpm  7052  findcard2  7078  findcard2s  7079  ac6sfi  7087  fiintim  7123  xpfi  7124  fidcenum  7155  ordiso  7235  ctmlemr  7307  ctm  7308  ctssdc  7312  pm54.43  7395  exmidfodomrlemim  7412  iftrueb01  7441  pw1m  7442  recclnq  7612  ltexnqq  7628  ltbtwnnqq  7635  recexprlemss1l  7855  recexprlemss1u  7856  negm  9849  ioom  10521  seq3f1olemp  10778  fiinfnf1o  11049  fihashf1rn  11051  climcau  11925  summodclem2  11961  zsumdc  11963  isumz  11968  fsumf1o  11969  fisumss  11971  fsumcl2lem  11977  fsumadd  11985  fsummulc2  12027  ntrivcvgap  12127  prodmodclem2  12156  zproddc  12158  prod1dc  12165  fprodf1o  12167  fprodssdc  12169  fprodmul  12170  nnmindc  12623  uzwodc  12626  pceu  12886  4sqlemafi  12986  4sqlem12  12993  ennnfone  13064  enctlem  13071  unct  13081  gsumfzval  13492  sgrpidmndm  13521  subrngintm  14245  subrgintm  14276  islssm  14390  lss0cl  14402  islidlm  14512  eltg3  14800  tgtop  14811  tgidm  14817  tgrest  14912  tgcn  14951  xblm  15160  dvfgg  15431  dvcnp2cntop  15442  2lgslem1  15839  pwtrufal  16649  gfsumval  16732