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  7377  ctmlemr  7449  ctm  7450  ctssdc  7454  pm54.43  7537  exmidfodomrlemim  7554  iftrueb01  7583  pw1m  7584  recclnq  7760  ltexnqq  7776  ltbtwnnqq  7783  recexprlemss1l  8003  recexprlemss1u  8004  negm  10025  ioom  10706  seq3f1olemp  10967  fiinfnf1o  11241  fihashf1rn  11243  hashf1  11303  climcau  12132  summodclem2  12168  zsumdc  12170  isumz  12175  fsumf1o  12176  fisumss  12178  fsumcl2lem  12184  fsumadd  12192  fsummulc2  12234  ntrivcvgap  12334  prodmodclem2  12363  zproddc  12365  prod1dc  12372  fprodf1o  12374  fprodssdc  12376  fprodmul  12377  nnmindc  12830  uzwodc  12833  pceu  13097  4sqlemafi  13197  4sqlem12  13204  ennnfone  13368  enctlem  13375  unct  13385  gzsumfzval  13764  sgrpidmndm  13786  gsumvalfi  14236  subrngintm  14604  subrgintm  14635  islssm  14778  lss0cl  14790  islidlm  14900  eltg3  15249  tgtop  15260  tgidm  15266  tgrest  15361  tgcn  15400  xblm  15609  dvfgg  15880  dvcnp2cntop  15891  2lgslem1  16376  pwtrufal  17193