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  4243  euotd  4299  ralxfr2d  4511  rexxfr2d  4512  releldmb  4915  relelrnb  4916  elres  4995  iss  5005  imain  5356  elunirn  5835  ovmpt4g  6068  oprssdmm  6257  op1steq  6265  fo2ndf  6313  reldmtpos  6339  rntpos  6343  tfrlemibacc  6412  tfrlemibxssdm  6413  tfrlemibfn  6414  tfrexlem  6420  tfr1onlembacc  6428  tfr1onlembxssdm  6429  tfr1onlembfn  6430  tfrcllembacc  6441  tfrcllembxssdm  6442  tfrcllembfn  6443  map0g  6775  xpdom3m  6929  phplem4  6952  phpm  6962  findcard2  6986  findcard2s  6987  ac6sfi  6995  fiintim  7028  xpfi  7029  fidcenum  7058  ordiso  7138  ctmlemr  7210  ctm  7211  ctssdc  7215  pm54.43  7298  exmidfodomrlemim  7309  recclnq  7505  ltexnqq  7521  ltbtwnnqq  7528  recexprlemss1l  7748  recexprlemss1u  7749  negm  9736  ioom  10403  seq3f1olemp  10660  fiinfnf1o  10931  fihashf1rn  10933  climcau  11658  summodclem2  11693  zsumdc  11695  isumz  11700  fsumf1o  11701  fisumss  11703  fsumcl2lem  11709  fsumadd  11717  fsummulc2  11759  ntrivcvgap  11859  prodmodclem2  11888  zproddc  11890  prod1dc  11897  fprodf1o  11899  fprodssdc  11901  fprodmul  11902  nnmindc  12355  uzwodc  12358  pceu  12618  4sqlemafi  12718  4sqlem12  12725  ennnfone  12796  enctlem  12803  unct  12813  gsumfzval  13223  sgrpidmndm  13252  subrngintm  13974  subrgintm  14005  islssm  14119  lss0cl  14131  islidlm  14241  eltg3  14529  tgtop  14540  tgidm  14546  tgrest  14641  tgcn  14680  xblm  14889  dvfgg  15160  dvcnp2cntop  15171  2lgslem1  15568  pwtrufal  15934