Theorem exlimdv 1867

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  1868  exlimdvv  1946  exlimddv  1947  tpid3g  3791  sssnm  3842  pwntru  4295  euotd  4353  ralxfr2d  4567  rexxfr2d  4568  reldmm  4956  releldmb  4975  relelrnb  4976  elres  5055  iss  5065  imain  5419  elunirn  5917  ovmpt4g  6154  oprssdmm  6343  op1steq  6351  fo2ndf  6401  reldmtpos  6462  rntpos  6466  tfrlemibacc  6535  tfrlemibxssdm  6536  tfrlemibfn  6537  tfrexlem  6543  tfr1onlembacc  6551  tfr1onlembxssdm  6552  tfr1onlembfn  6553  tfrcllembacc  6564  tfrcllembxssdm  6565  tfrcllembfn  6566  map0g  6900  dom1o  7045  xpdom3m  7061  phplem4  7084  phpm  7095  findcard2  7121  findcard2s  7122  ac6sfi  7130  fiintim  7166  xpfi  7167  fidcenum  7198  ordiso  7295  ctmlemr  7367  ctm  7368  ctssdc  7372  pm54.43  7455  exmidfodomrlemim  7472  iftrueb01  7501  pw1m  7502  recclnq  7672  ltexnqq  7688  ltbtwnnqq  7695  recexprlemss1l  7915  recexprlemss1u  7916  negm  9910  ioom  10583  seq3f1olemp  10840  fiinfnf1o  11111  fihashf1rn  11113  climcau  11987  summodclem2  12023  zsumdc  12025  isumz  12030  fsumf1o  12031  fisumss  12033  fsumcl2lem  12039  fsumadd  12047  fsummulc2  12089  ntrivcvgap  12189  prodmodclem2  12218  zproddc  12220  prod1dc  12227  fprodf1o  12229  fprodssdc  12231  fprodmul  12232  nnmindc  12685  uzwodc  12688  pceu  12948  4sqlemafi  13048  4sqlem12  13055  ennnfone  13126  enctlem  13133  unct  13143  gsumfzval  13554  sgrpidmndm  13583  subrngintm  14307  subrgintm  14338  islssm  14453  lss0cl  14465  islidlm  14575  eltg3  14868  tgtop  14879  tgidm  14885  tgrest  14980  tgcn  15019  xblm  15228  dvfgg  15499  dvcnp2cntop  15510  2lgslem1  15910  pwtrufal  16719  gfsumval  16809