Theorem rexlimdvw 2608

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

Syntax hints:   -> wi 4   e. wcel 2158   E.wrex 2466

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 1457  ax-gen 1459  ax-ie1 1503  ax-ie2 1504  ax-4 1520  ax-17 1536  ax-ial 1544  ax-i5r 1545

This theorem depends on definitions:  df-bi 117  df-nf 1471  df-ral 2470  df-rex 2471

This theorem is referenced by:  nnpredcl  4634  qsss  6608  fodjuomnilemdc  7156  ltpopr  7608  ltsopr  7609  ltexprlemlol  7615  ltexprlemupu  7617  cauappcvgprlemrnd  7663  caucvgprlemrnd  7686  caucvgprprlemrnd  7714  suplocexprlemss  7728  suplocexprlemrl  7730  suplocsrlempr  7820  climuni  11315  lspsnel  13606  cncnp2m  14027  bj-findis  15027