Theorem exlimdv 1843

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

Syntax hints:   -> wi 4   E.wex 1516

This theorem was proved from axioms:  ax-mp 5  ax-1 6  ax-2 7  ax-ia1 106  ax-5 1471  ax-gen 1473  ax-ie2 1518  ax-17 1550

This theorem depends on definitions:  df-bi 117

This theorem is referenced by:  ax11v2  1844  exlimdvv  1922  exlimddv  1923  tpid3g  3758  sssnm  3808  pwntru  4259  euotd  4317  ralxfr2d  4529  rexxfr2d  4530  releldmb  4934  relelrnb  4935  elres  5014  iss  5024  imain  5375  elunirn  5858  ovmpt4g  6091  oprssdmm  6280  op1steq  6288  fo2ndf  6336  reldmtpos  6362  rntpos  6366  tfrlemibacc  6435  tfrlemibxssdm  6436  tfrlemibfn  6437  tfrexlem  6443  tfr1onlembacc  6451  tfr1onlembxssdm  6452  tfr1onlembfn  6453  tfrcllembacc  6464  tfrcllembxssdm  6465  tfrcllembfn  6466  map0g  6798  xpdom3m  6954  phplem4  6977  phpm  6988  findcard2  7012  findcard2s  7013  ac6sfi  7021  fiintim  7054  xpfi  7055  fidcenum  7084  ordiso  7164  ctmlemr  7236  ctm  7237  ctssdc  7241  pm54.43  7324  exmidfodomrlemim  7340  iftrueb01  7369  pw1m  7370  recclnq  7540  ltexnqq  7556  ltbtwnnqq  7563  recexprlemss1l  7783  recexprlemss1u  7784  negm  9771  ioom  10440  seq3f1olemp  10697  fiinfnf1o  10968  fihashf1rn  10970  climcau  11773  summodclem2  11808  zsumdc  11810  isumz  11815  fsumf1o  11816  fisumss  11818  fsumcl2lem  11824  fsumadd  11832  fsummulc2  11874  ntrivcvgap  11974  prodmodclem2  12003  zproddc  12005  prod1dc  12012  fprodf1o  12014  fprodssdc  12016  fprodmul  12017  nnmindc  12470  uzwodc  12473  pceu  12733  4sqlemafi  12833  4sqlem12  12840  ennnfone  12911  enctlem  12918  unct  12928  gsumfzval  13338  sgrpidmndm  13367  subrngintm  14089  subrgintm  14120  islssm  14234  lss0cl  14246  islidlm  14356  eltg3  14644  tgtop  14655  tgidm  14661  tgrest  14756  tgcn  14795  xblm  15004  dvfgg  15275  dvcnp2cntop  15286  2lgslem1  15683  dom1o  16128  pwtrufal  16136