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  4336  euotd  4395  ralxfr2d  4610  rexxfr2d  4611  reldmm  5000  releldmb  5019  relelrnb  5020  elres  5099  iss  5109  imain  5463  elunirn  5972  ovmpt4g  6211  oprssdmm  6405  op1steq  6413  fo2ndf  6463  reldmtpos  6524  rntpos  6528  tfrlemibacc  6597  tfrlemibxssdm  6598  tfrlemibfn  6599  tfrexlem  6605  tfr1onlembacc  6613  tfr1onlembxssdm  6614  tfr1onlembfn  6615  tfrcllembacc  6626  tfrcllembxssdm  6627  tfrcllembfn  6628  map0g  6969  dom1o  7116  xpdom3m  7132  phplem4  7156  phpm  7167  findcard2  7193  findcard2s  7194  ac6sfi  7202  fiintim  7238  xpfi  7239  fidcenum  7273  ordiso  7376  ctmlemr  7448  ctm  7449  ctssdc  7453  pm54.43  7536  exmidfodomrlemim  7553  iftrueb01  7582  pw1m  7583  recclnq  7759  ltexnqq  7775  ltbtwnnqq  7782  recexprlemss1l  8002  recexprlemss1u  8003  negm  10024  ioom  10705  seq3f1olemp  10965  fiinfnf1o  11239  fihashf1rn  11241  hashf1  11301  climcau  12129  summodclem2  12165  zsumdc  12167  isumz  12172  fsumf1o  12173  fisumss  12175  fsumcl2lem  12181  fsumadd  12189  fsummulc2  12231  ntrivcvgap  12331  prodmodclem2  12360  zproddc  12362  prod1dc  12369  fprodf1o  12371  fprodssdc  12373  fprodmul  12374  nnmindc  12827  uzwodc  12830  pceu  13094  4sqlemafi  13194  4sqlem12  13201  ennnfone  13365  enctlem  13372  unct  13382  gzsumfzval  13760  sgrpidmndm  13782  gsumvalfi  14201  subrngintm  14569  subrgintm  14600  islssm  14743  lss0cl  14755  islidlm  14865  eltg3  15207  tgtop  15218  tgidm  15224  tgrest  15319  tgcn  15358  xblm  15567  dvfgg  15838  dvcnp2cntop  15849  2lgslem1  16308  pwtrufal  17125