Theorem exlimdv 1872

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

This proof depends on syntax axioms:   -> wi 4   E.wex 1545

This proof depends on axioms:  ax-mp 5  ax-1 6  ax-2 7  ax-ia1 106  ax-5 1500  ax-gen 1502  ax-ie2 1547  ax-17 1579

This proof depends on definitions:  df-bi 117

This theorem is used by:  ax11v2  1873  exlimdvv  1953  exlimddv  1954  tpid3g  3828  sssnm  3879  pwntru  4338  euotd  4397  ralxfr2d  4612  rexxfr2d  4613  reldmm  5002  releldmb  5021  relelrnb  5022  elres  5101  iss  5112  imain  5466  elunirn  5975  ovmpt4g  6214  oprssdmm  6409  op1steq  6417  fo2ndf  6467  reldmtpos  6528  rntpos  6532  tfrlemibacc  6601  tfrlemibxssdm  6602  tfrlemibfn  6603  tfrexlem  6609  tfr1onlembacc  6617  tfr1onlembxssdm  6618  tfr1onlembfn  6619  tfrcllembacc  6630  tfrcllembxssdm  6631  tfrcllembfn  6632  map0g  6973  dom1o  7120  xpdom3m  7136  phplem4  7160  phpm  7171  findcard2  7197  findcard2s  7198  ac6sfi  7206  fiintim  7242  xpfi  7243  fidcenum  7278  ordiso  7382  ctmlemr  7454  ctm  7455  ctssdc  7459  pm54.43  7542  exmidfodomrlemim  7559  iftrueb01  7588  pw1m  7589  recclnq  7765  ltexnqq  7781  ltbtwnnqq  7788  recexprlemss1l  8008  recexprlemss1u  8009  negm  10031  ioom  10712  seq3f1olemp  10973  fiinfnf1o  11247  fihashf1rn  11249  hashf1  11309  climcau  12138  summodclem2  12174  zsumdc  12176  isumz  12181  fsumf1o  12182  fisumss  12184  fsumcl2lem  12190  fsumadd  12198  fsummulc2  12240  ntrivcvgap  12340  prodmodclem2  12369  zproddc  12371  prod1dc  12378  fprodf1o  12380  fprodssdc  12382  fprodmul  12383  nnmindc  12836  uzwodc  12839  pceu  13103  4sqlemafi  13203  4sqlem12  13210  ennnfone  13374  enctlem  13381  unct  13391  gzsumfzval  13770  sgrpidmndm  13792  gsumvalfi  14242  gsum2d2fi  14274  subrngintm  14629  subrgintm  14660  islssm  14803  lss0cl  14815  islidlm  14925  eltg3  15283  tgtop  15294  tgidm  15300  tgrest  15395  tgcn  15434  xblm  15643  dvfgg  15914  dvcnp2cntop  15925  2lgslem1  16415  pwtrufal  17232