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  3734  sssnm  3781  pwntru  4229  euotd  4284  ralxfr2d  4496  rexxfr2d  4497  releldmb  4900  relelrnb  4901  elres  4979  iss  4989  imain  5337  elunirn  5810  ovmpt4g  6042  oprssdmm  6226  op1steq  6234  fo2ndf  6282  reldmtpos  6308  rntpos  6312  tfrlemibacc  6381  tfrlemibxssdm  6382  tfrlemibfn  6383  tfrexlem  6389  tfr1onlembacc  6397  tfr1onlembxssdm  6398  tfr1onlembfn  6399  tfrcllembacc  6410  tfrcllembxssdm  6411  tfrcllembfn  6412  map0g  6744  xpdom3m  6890  phplem4  6913  phpm  6923  findcard2  6947  findcard2s  6948  ac6sfi  6956  fiintim  6987  xpfi  6988  fidcenum  7017  ordiso  7097  ctmlemr  7169  ctm  7170  ctssdc  7174  pm54.43  7252  exmidfodomrlemim  7263  recclnq  7454  ltexnqq  7470  ltbtwnnqq  7477  recexprlemss1l  7697  recexprlemss1u  7698  negm  9683  ioom  10332  seq3f1olemp  10589  fiinfnf1o  10860  fihashf1rn  10862  climcau  11493  summodclem2  11528  zsumdc  11530  isumz  11535  fsumf1o  11536  fisumss  11538  fsumcl2lem  11544  fsumadd  11552  fsummulc2  11594  ntrivcvgap  11694  prodmodclem2  11723  zproddc  11725  prod1dc  11732  fprodf1o  11734  fprodssdc  11736  fprodmul  11737  nnmindc  12174  uzwodc  12177  pceu  12436  4sqlemafi  12536  4sqlem12  12543  ennnfone  12585  enctlem  12592  unct  12602  gsumfzval  12977  sgrpidmndm  13004  subrngintm  13711  subrgintm  13742  islssm  13856  lss0cl  13868  islidlm  13978  eltg3  14236  tgtop  14247  tgidm  14253  tgrest  14348  tgcn  14387  xblm  14596  dvfgg  14867  dvcnp2cntop  14878  2lgslem1  15248  pwtrufal  15558