Theorem exlimdv 1865

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

Syntax hints:   -> wi 4   E.wex 1538

This theorem was proved from axioms:  ax-mp 5  ax-1 6  ax-2 7  ax-ia1 106  ax-5 1493  ax-gen 1495  ax-ie2 1540  ax-17 1572

This theorem depends on definitions:  df-bi 117

This theorem is referenced by:  ax11v2  1866  exlimdvv  1944  exlimddv  1945  tpid3g  3782  sssnm  3832  pwntru  4283  euotd  4341  ralxfr2d  4555  rexxfr2d  4556  reldmm  4942  releldmb  4961  relelrnb  4962  elres  5041  iss  5051  imain  5403  elunirn  5890  ovmpt4g  6127  oprssdmm  6317  op1steq  6325  fo2ndf  6373  reldmtpos  6399  rntpos  6403  tfrlemibacc  6472  tfrlemibxssdm  6473  tfrlemibfn  6474  tfrexlem  6480  tfr1onlembacc  6488  tfr1onlembxssdm  6489  tfr1onlembfn  6490  tfrcllembacc  6501  tfrcllembxssdm  6502  tfrcllembfn  6503  map0g  6835  dom1o  6977  xpdom3m  6993  phplem4  7016  phpm  7027  findcard2  7051  findcard2s  7052  ac6sfi  7060  fiintim  7093  xpfi  7094  fidcenum  7123  ordiso  7203  ctmlemr  7275  ctm  7276  ctssdc  7280  pm54.43  7363  exmidfodomrlemim  7379  iftrueb01  7408  pw1m  7409  recclnq  7579  ltexnqq  7595  ltbtwnnqq  7602  recexprlemss1l  7822  recexprlemss1u  7823  negm  9810  ioom  10480  seq3f1olemp  10737  fiinfnf1o  11008  fihashf1rn  11010  climcau  11858  summodclem2  11893  zsumdc  11895  isumz  11900  fsumf1o  11901  fisumss  11903  fsumcl2lem  11909  fsumadd  11917  fsummulc2  11959  ntrivcvgap  12059  prodmodclem2  12088  zproddc  12090  prod1dc  12097  fprodf1o  12099  fprodssdc  12101  fprodmul  12102  nnmindc  12555  uzwodc  12558  pceu  12818  4sqlemafi  12918  4sqlem12  12925  ennnfone  12996  enctlem  13003  unct  13013  gsumfzval  13424  sgrpidmndm  13453  subrngintm  14176  subrgintm  14207  islssm  14321  lss0cl  14333  islidlm  14443  eltg3  14731  tgtop  14742  tgidm  14748  tgrest  14843  tgcn  14882  xblm  15091  dvfgg  15362  dvcnp2cntop  15373  2lgslem1  15770  pwtrufal  16363