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  1947  exlimddv  1948  tpid3g  3806  sssnm  3857  pwntru  4311  euotd  4370  ralxfr2d  4584  rexxfr2d  4585  reldmm  4974  releldmb  4993  relelrnb  4994  elres  5073  iss  5083  imain  5437  elunirn  5938  ovmpt4g  6175  oprssdmm  6364  op1steq  6372  fo2ndf  6422  reldmtpos  6483  rntpos  6487  tfrlemibacc  6556  tfrlemibxssdm  6557  tfrlemibfn  6558  tfrexlem  6564  tfr1onlembacc  6572  tfr1onlembxssdm  6573  tfr1onlembfn  6574  tfrcllembacc  6585  tfrcllembxssdm  6586  tfrcllembfn  6587  map0g  6921  dom1o  7068  xpdom3m  7084  phplem4  7108  phpm  7119  findcard2  7145  findcard2s  7146  ac6sfi  7154  fiintim  7190  xpfi  7191  fidcenum  7225  ordiso  7326  ctmlemr  7398  ctm  7399  ctssdc  7403  pm54.43  7486  exmidfodomrlemim  7503  iftrueb01  7532  pw1m  7533  recclnq  7706  ltexnqq  7722  ltbtwnnqq  7729  recexprlemss1l  7949  recexprlemss1u  7950  negm  9946  ioom  10619  seq3f1olemp  10876  fiinfnf1o  11147  fihashf1rn  11149  climcau  12028  summodclem2  12064  zsumdc  12066  isumz  12071  fsumf1o  12072  fisumss  12074  fsumcl2lem  12080  fsumadd  12088  fsummulc2  12130  ntrivcvgap  12230  prodmodclem2  12259  zproddc  12261  prod1dc  12268  fprodf1o  12270  fprodssdc  12272  fprodmul  12273  nnmindc  12726  uzwodc  12729  pceu  12989  4sqlemafi  13089  4sqlem12  13096  ennnfone  13168  enctlem  13175  unct  13185  gsumfzval  13596  sgrpidmndm  13625  subrngintm  14349  subrgintm  14380  islssm  14497  lss0cl  14509  islidlm  14619  eltg3  14914  tgtop  14925  tgidm  14931  tgrest  15026  tgcn  15065  xblm  15274  dvfgg  15545  dvcnp2cntop  15556  2lgslem1  15956  pwtrufal  16763  gfsumval  16853