Theorem rexlimdv 2432

Description: Inference from Theorem 19.23 of [Margaris] p. 90 (restricted quantifier version). (Contributed by NM, 14-Nov-2002.) (Proof shortened by Eric Schmidt, 22-Dec-2006.)

Hypothesis

Ref	Expression
rexlimdv.1	|- ( ph -> ( x e. A -> ( ps -> ch ) ) )

Assertion

Ref	Expression
rexlimdv	|- ( ph -> ( E. x e. A ps -> ch ) )

Distinct variable groups:   ph, x   ch, x

Allowed substitution hints:   ps( x)   A( x)

Proof of Theorem rexlimdv

Step	Hyp	Ref	Expression
1		nfv 1421	. 2 |- F/ x ph
2		nfv 1421	. 2 |- F/ x ch
3		rexlimdv.1	. 2 |- ( ph -> ( x e. A -> ( ps -> ch ) ) )
4	1, 2, 3	rexlimd 2430	1 |- ( ph -> ( E. x e. A ps -> ch ) )

Syntax hints:   -> wi 4   e. wcel 1393   E.wrex 2307

This theorem was proved from axioms:  ax-1 5  ax-2 6  ax-mp 7  ax-ia1 99  ax-ia2 100  ax-ia3 101  ax-5 1336  ax-gen 1338  ax-ie1 1382  ax-ie2 1383  ax-4 1400  ax-17 1419  ax-ial 1427  ax-i5r 1428

This theorem depends on definitions:  df-bi 110  df-nf 1350  df-ral 2311  df-rex 2312

This theorem is referenced by:  rexlimdva  2433  rexlimdv3a  2435  rexlimdvw  2436  rexlimdvv  2439  trintssm  3870  ssorduni  4213  funcnvuni  4968  dffo3  5314  smoiun  5916  tfrlem9  5935  ordiso2  6357  axprecex  6954  recexap  7634  zdiv  8328  btwnz  8357  lbzbi  8551