Theorem rexlimdvv 2630

Description: Inference from Theorem 19.23 of [Margaris] p. 90. (Restricted quantifier version.) (Contributed by NM, 22-Jul-2004.)

Hypothesis

Ref	Expression
rexlimdvv.1	|- ( ph -> ( ( x e. A /\ y e. B ) -> ( ps -> ch ) ) )

Assertion

Ref	Expression
rexlimdvv	|- ( ph -> ( E. x e. A E. y e. B ps -> ch ) )

Distinct variable groups:   x, y, ph   ch, x, y   y, A

Allowed substitution hints:   ps( x, y)   A( x)   B( x, y)

Proof of Theorem rexlimdvv

Step	Hyp	Ref	Expression
1		rexlimdvv.1	. . . 4 |- ( ph -> ( ( x e. A /\ y e. B ) -> ( ps -> ch ) ) )
2	1	expdimp 259	. . 3 |- ( ( ph /\ x e. A ) -> ( y e. B -> ( ps -> ch ) ) )
3	2	rexlimdv 2622	. 2 |- ( ( ph /\ x e. A ) -> ( E. y e. B ps -> ch ) )
4	3	rexlimdva 2623	1 |- ( ph -> ( E. x e. A E. y e. B ps -> ch ) )

Syntax hints:   -> wi 4   /\ wa 104   e. wcel 2176   E.wrex 2485

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 1470  ax-gen 1472  ax-ie1 1516  ax-ie2 1517  ax-4 1533  ax-17 1549  ax-ial 1557  ax-i5r 1558

This theorem depends on definitions:  df-bi 117  df-nf 1484  df-ral 2489  df-rex 2490

This theorem is referenced by:  rexlimdvva  2631  f1oiso2  5896  rex2dom  6910  xpdom2  6926  genpcdl  7632  genpcuu  7633  distrlem1prl  7695  distrlem1pru  7696  distrlem5prl  7699  distrlem5pru  7700  recexprlemss1l  7748  recexprlemss1u  7749  qaddcl  9756  qmulcl  9758  summodc  11694  dvdsgcd  12333  gcddiv  12340  pceu  12618  pcqcl  12629  txcnp  14743  blssps  14899  blss  14900  tgqioo  15027