Theorem rexlimdvw 2615

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

Syntax hints:   -> wi 4   e. wcel 2164   E.wrex 2473

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 1458  ax-gen 1460  ax-ie1 1504  ax-ie2 1505  ax-4 1521  ax-17 1537  ax-ial 1545  ax-i5r 1546

This theorem depends on definitions:  df-bi 117  df-nf 1472  df-ral 2477  df-rex 2478

This theorem is referenced by:  nnpredcl  4655  qsss  6648  fodjuomnilemdc  7203  ltpopr  7655  ltsopr  7656  ltexprlemlol  7662  ltexprlemupu  7664  cauappcvgprlemrnd  7710  caucvgprlemrnd  7733  caucvgprprlemrnd  7761  suplocexprlemss  7775  suplocexprlemrl  7777  suplocsrlempr  7867  climuni  11436  ellspsn  13913  cncnp2m  14399  bj-findis  15471