Theorem rexlimdvw 2958

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 2953	1 |- ( ph -> ( E. x e. A ps -> ch ) )

Syntax hints:   -> wi 4   e. wcel 1767   E.wrex 2815

This theorem was proved from axioms:  ax-mp 5  ax-1 6  ax-2 7  ax-3 8  ax-gen 1601  ax-4 1612  ax-5 1680

This theorem depends on definitions:  df-bi 185  df-an 371  df-ex 1597  df-ral 2819  df-rex 2820

This theorem is referenced by:  odi  7225  omeulem1  7228  qsss  7369  findcard3  7759  r1pwss  8198  dfac5lem4  8503  climuni  13331  rlimno1  13432  caurcvg2  13456  sscfn1  15040  gsumval2a  15822  gsumval3OLD  16696  gsumval3  16699  opnnei  19384  dislly  19761  txcmplem1  19874  ufileu  20152  alexsubALT  20283  metustelOLD  20786  metustel  20787  metustfbasOLD  20800  metustfbas  20801  i1faddlem  21832  ulmval  22506  brbtwn  23875  wwlknredwwlkn0  24400  iseupa  24638  numclwwlkun  24753  iccllyscon  28332  cvmopnlem  28360  cvmlift2lem10  28394  cvmlift3lem8  28408  lfinpfin  29773  sdclem2  29836  heibor1lem  29906  elrfi  30228  eldiophb  30292  dnnumch2  30595