Theorem exlimdv 1830

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

Syntax hints:   -> wi 4   E.wex 1503

This theorem was proved from axioms:  ax-mp 5  ax-1 6  ax-2 7  ax-ia1 106  ax-5 1458  ax-gen 1460  ax-ie2 1505  ax-17 1537

This theorem depends on definitions:  df-bi 117

This theorem is referenced by:  ax11v2  1831  exlimdvv  1909  exlimddv  1910  tpid3g  3733  sssnm  3780  pwntru  4228  euotd  4283  ralxfr2d  4495  rexxfr2d  4496  releldmb  4899  relelrnb  4900  elres  4978  iss  4988  imain  5336  elunirn  5809  ovmpt4g  6041  oprssdmm  6224  op1steq  6232  fo2ndf  6280  reldmtpos  6306  rntpos  6310  tfrlemibacc  6379  tfrlemibxssdm  6380  tfrlemibfn  6381  tfrexlem  6387  tfr1onlembacc  6395  tfr1onlembxssdm  6396  tfr1onlembfn  6397  tfrcllembacc  6408  tfrcllembxssdm  6409  tfrcllembfn  6410  map0g  6742  xpdom3m  6888  phplem4  6911  phpm  6921  findcard2  6945  findcard2s  6946  ac6sfi  6954  fiintim  6985  xpfi  6986  fidcenum  7015  ordiso  7095  ctmlemr  7167  ctm  7168  ctssdc  7172  pm54.43  7250  exmidfodomrlemim  7261  recclnq  7452  ltexnqq  7468  ltbtwnnqq  7475  recexprlemss1l  7695  recexprlemss1u  7696  negm  9680  ioom  10329  seq3f1olemp  10586  fiinfnf1o  10857  fihashf1rn  10859  climcau  11490  summodclem2  11525  zsumdc  11527  isumz  11532  fsumf1o  11533  fisumss  11535  fsumcl2lem  11541  fsumadd  11549  fsummulc2  11591  ntrivcvgap  11691  prodmodclem2  11720  zproddc  11722  prod1dc  11729  fprodf1o  11731  fprodssdc  11733  fprodmul  11734  nnmindc  12171  uzwodc  12174  pceu  12433  4sqlemafi  12533  4sqlem12  12540  ennnfone  12582  enctlem  12589  unct  12599  gsumfzval  12974  sgrpidmndm  13001  subrngintm  13708  subrgintm  13739  islssm  13853  lss0cl  13865  islidlm  13975  eltg3  14225  tgtop  14236  tgidm  14242  tgrest  14337  tgcn  14376  xblm  14585  dvfgg  14842  dvcnp2cntop  14848  pwtrufal  15488