Theorem rexlimdvw 2834

Description: Inference from Theorem 19.23 of [Margaris] p. 90 (restricted quantifier version). (Contributed by NM, 18-Jun-2014.)

Hypothesis

Ref	Expression
rexlimdvw.1	|- ( ph -> ( ps -> ch ) )

Assertion

Ref	Expression
rexlimdvw	|- ( ph -> ( E. x e. A ps -> ch ) )

Distinct variable groups:   ph, x   ch, x

Allowed substitution hints:   ps( x)   A( x)

Proof of Theorem rexlimdvw

Step	Hyp	Ref	Expression
1		rexlimdvw.1	. . 3 |- ( ph -> ( ps -> ch ) )
2	1	a1d 25	. 2 |- ( ph -> ( x e. A -> ( ps -> ch ) ) )
3	2	rexlimdv 2830	1 |- ( ph -> ( E. x e. A ps -> ch ) )

Syntax hints:   -> wi 4   e. wcel 1755   E.wrex 2706

This theorem was proved from axioms:  ax-mp 5  ax-1 6  ax-2 7  ax-3 8  ax-gen 1594  ax-4 1605  ax-5 1669  ax-6 1707  ax-7 1727  ax-10 1774  ax-12 1791

This theorem depends on definitions:  df-bi 185  df-an 371  df-ex 1590  df-nf 1593  df-ral 2710  df-rex 2711

This theorem is referenced by:  odi  7006  omeulem1  7009  qsss  7149  findcard3  7543  r1pwss  7979  dfac5lem4  8284  climuni  13014  rlimno1  13115  caurcvg2  13139  sscfn1  14713  gsumval2a  15492  gsumval3OLD  16362  gsumval3  16365  opnnei  18566  dislly  18943  txcmplem1  19056  ufileu  19334  alexsubALT  19465  metustelOLD  19968  metustel  19969  metustfbasOLD  19982  metustfbas  19983  i1faddlem  21013  ulmval  21730  brbtwn  22968  iseupa  23409  iccllyscon  26987  cvmopnlem  27015  cvmlift2lem10  27049  cvmlift3lem8  27063  lfinpfin  28419  sdclem2  28482  heibor1lem  28552  elrfi  28875  eldiophb  28940  dnnumch2  29243  wwlknredwwlkn0  30205  numclwwlkun  30518