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  6529  rntpos  6533  tfrlemibacc  6602  tfrlemibxssdm  6603  tfrlemibfn  6604  tfrexlem  6610  tfr1onlembacc  6618  tfr1onlembxssdm  6619  tfr1onlembfn  6620  tfrcllembacc  6631  tfrcllembxssdm  6632  tfrcllembfn  6633  map0g  6974  dom1o  7122  xpdom3m  7138  phplem4  7162  phpm  7173  findcard2  7199  findcard2s  7200  ac6sfi  7208  fiintim  7244  xpfi  7245  fidcenum  7280  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  10030  ioom  10711  seq3f1olemp  10972  fiinfnf1o  11246  fihashf1rn  11248  hashf1  11308  climcau  12137  summodclem2  12173  zsumdc  12175  isumz  12180  fsumf1o  12181  fisumss  12183  fsumcl2lem  12189  fsumadd  12197  fsummulc2  12239  ntrivcvgap  12339  prodmodclem2  12368  zproddc  12370  prod1dc  12377  fprodf1o  12379  fprodssdc  12381  fprodmul  12382  nnmindc  12835  uzwodc  12838  pceu  13102  4sqlemafi  13202  4sqlem12  13209  ennnfone  13373  enctlem  13380  unct  13390  gzsumfzval  13769  sgrpidmndm  13791  gsumvalfi  14241  gsum2d2fi  14273  subrngintm  14628  subrgintm  14659  islssm  14802  lss0cl  14814  islidlm  14924  eltg3  15300  tgtop  15311  tgidm  15317  tgrest  15412  tgcn  15451  xblm  15660  dvfgg  15931  dvcnp2cntop  15942  2lgslem1  16432  pwtrufal  17249