Theorem rexlimdvv 2618

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

Syntax hints:   -> wi 4   /\ wa 104   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:  rexlimdvva  2619  f1oiso2  5870  xpdom2  6885  genpcdl  7579  genpcuu  7580  distrlem1prl  7642  distrlem1pru  7643  distrlem5prl  7646  distrlem5pru  7647  recexprlemss1l  7695  recexprlemss1u  7696  qaddcl  9700  qmulcl  9702  summodc  11526  dvdsgcd  12149  gcddiv  12156  pceu  12433  pcqcl  12444  txcnp  14439  blssps  14595  blss  14596  tgqioo  14715