Theorem rexlimdvv 2675

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 2667	. 2 |- ( ( ph /\ x e. A ) -> ( E. y e. B ps -> ch ) )
4	3	rexlimdva 2668	1 |- ( ph -> ( E. x e. A E. y e. B ps -> ch ) )

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

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 1500  ax-gen 1502  ax-ie1 1546  ax-ie2 1547  ax-4 1563  ax-17 1579  ax-ial 1587  ax-i5r 1588

This theorem depends on definitions:  df-bi 117  df-nf 1514  df-ral 2533  df-rex 2534

This theorem is referenced by:  rexlimdvva  2676  f1oiso2  6023  rex2dom  7100  xpdom2  7119  genpcdl  7876  genpcuu  7877  distrlem1prl  7939  distrlem1pru  7940  distrlem5prl  7943  distrlem5pru  7944  recexprlemss1l  7992  recexprlemss1u  7993  qaddcl  10014  qmulcl  10016  summodc  12128  dvdsgcd  12767  gcddiv  12774  pceu  13052  pcqcl  13063  txcnp  15295  blssps  15451  blss  15452  tgqioo  15579  upgredg2vtx  16303