Theorem rexlimdvw 2628

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

Syntax hints:   -> wi 4   e. wcel 2177   E.wrex 2486

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 1471  ax-gen 1473  ax-ie1 1517  ax-ie2 1518  ax-4 1534  ax-17 1550  ax-ial 1558  ax-i5r 1559

This theorem depends on definitions:  df-bi 117  df-nf 1485  df-ral 2490  df-rex 2491

This theorem is referenced by:  nnpredcl  4679  qsss  6694  fodjuomnilemdc  7261  ltpopr  7728  ltsopr  7729  ltexprlemlol  7735  ltexprlemupu  7737  cauappcvgprlemrnd  7783  caucvgprlemrnd  7806  caucvgprprlemrnd  7834  suplocexprlemss  7848  suplocexprlemrl  7850  suplocsrlempr  7940  climuni  11679  ellspsn  14254  cncnp2m  14778  bj-findis  16053