Theorem exlimdv 1833

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

Syntax hints:   -> wi 4   E.wex 1506

This theorem was proved from axioms:  ax-mp 5  ax-1 6  ax-2 7  ax-ia1 106  ax-5 1461  ax-gen 1463  ax-ie2 1508  ax-17 1540

This theorem depends on definitions:  df-bi 117

This theorem is referenced by:  ax11v2  1834  exlimdvv  1912  exlimddv  1913  tpid3g  3738  sssnm  3785  pwntru  4233  euotd  4288  ralxfr2d  4500  rexxfr2d  4501  releldmb  4904  relelrnb  4905  elres  4983  iss  4993  imain  5341  elunirn  5814  ovmpt4g  6047  oprssdmm  6231  op1steq  6239  fo2ndf  6287  reldmtpos  6313  rntpos  6317  tfrlemibacc  6386  tfrlemibxssdm  6387  tfrlemibfn  6388  tfrexlem  6394  tfr1onlembacc  6402  tfr1onlembxssdm  6403  tfr1onlembfn  6404  tfrcllembacc  6415  tfrcllembxssdm  6416  tfrcllembfn  6417  map0g  6749  xpdom3m  6895  phplem4  6918  phpm  6928  findcard2  6952  findcard2s  6953  ac6sfi  6961  fiintim  6994  xpfi  6995  fidcenum  7024  ordiso  7104  ctmlemr  7176  ctm  7177  ctssdc  7181  pm54.43  7260  exmidfodomrlemim  7271  recclnq  7462  ltexnqq  7478  ltbtwnnqq  7485  recexprlemss1l  7705  recexprlemss1u  7706  negm  9692  ioom  10353  seq3f1olemp  10610  fiinfnf1o  10881  fihashf1rn  10883  climcau  11515  summodclem2  11550  zsumdc  11552  isumz  11557  fsumf1o  11558  fisumss  11560  fsumcl2lem  11566  fsumadd  11574  fsummulc2  11616  ntrivcvgap  11716  prodmodclem2  11745  zproddc  11747  prod1dc  11754  fprodf1o  11756  fprodssdc  11758  fprodmul  11759  nnmindc  12212  uzwodc  12215  pceu  12475  4sqlemafi  12575  4sqlem12  12582  ennnfone  12653  enctlem  12660  unct  12670  gsumfzval  13060  sgrpidmndm  13087  subrngintm  13794  subrgintm  13825  islssm  13939  lss0cl  13951  islidlm  14061  eltg3  14319  tgtop  14330  tgidm  14336  tgrest  14431  tgcn  14470  xblm  14679  dvfgg  14950  dvcnp2cntop  14961  2lgslem1  15358  pwtrufal  15670