Theorem rexlimdvw 2672

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 22	. 2 |- ( ph -> ( x e. A -> ( ps -> ch ) ) )
3	2	rexlimdv 2667	1 |- ( ph -> ( E. x e. A ps -> ch ) )

Syntax hints:   -> wi 4   e. wcel 2209   E.wrex 2529

This theorem was proved from axioms:  ax-mp 5  ax-1 6  ax-2 7  ax-ia1 106  ax-ia2 107  ax-ia3 108  ax-5 1500  ax-gen 1502  ax-ie1 1546  ax-ie2 1547  ax-4 1563  ax-17 1579  ax-ial 1587  ax-i5r 1588

This theorem depends on definitions:  df-bi 117  df-nf 1514  df-ral 2533  df-rex 2534

This theorem is referenced by:  nnpredcl  4765  qsss  6858  fodjuomnilemdc  7474  ltpopr  7952  ltsopr  7953  ltexprlemlol  7959  ltexprlemupu  7961  cauappcvgprlemrnd  8007  caucvgprlemrnd  8030  caucvgprprlemrnd  8058  suplocexprlemss  8072  suplocexprlemrl  8074  suplocsrlempr  8164  climuni  12037  ellspsn  14726  cncnp2m  15255  bj-findis  16919