Theorem rexlimivv 2600

Description: Inference from Theorem 19.23 of [Margaris] p. 90 (restricted quantifier version). (Contributed by NM, 17-Feb-2004.)

Hypothesis

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

Assertion

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

Distinct variable groups:   x, y, ps   y, A

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

Proof of Theorem rexlimivv

Step	Hyp	Ref	Expression
1		rexlimivv.1	. . 3 |- ( ( x e. A /\ y e. B ) -> ( ph -> ps ) )
2	1	rexlimdva 2594	. 2 |- ( x e. A -> ( E. y e. B ph -> ps ) )
3	2	rexlimiv 2588	1 |- ( E. x e. A E. y e. B ph -> ps )

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

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 1447  ax-gen 1449  ax-ie1 1493  ax-ie2 1494  ax-4 1510  ax-17 1526  ax-ial 1534  ax-i5r 1535

This theorem depends on definitions:  df-bi 117  df-nf 1461  df-ral 2460  df-rex 2461

This theorem is referenced by:  opelxp  4657  f1o2ndf1  6229  xpdom2  6831  distrlem5prl  7585  distrlem5pru  7586  mulrid  7954  cnegex  8135  recexap  8610  creur  8916  creui  8917  cju  8918  elz2  9324  qre  9625  qaddcl  9635  qnegcl  9636  qmulcl  9637  qreccl  9642  elpqb  9649  replim  10868  prodmodc  11586  odd2np1  11878  opoe  11900  omoe  11901  opeo  11902  omeo  11903  qredeu  12097  pythagtriplem1  12265  pcz  12331  4sqlem1  12386  4sqlem2  12387  4sqlem4  12390  mul4sq  12392  txuni2  13759  blssioo  14048  tgioo  14049  2sqlem2  14465  mul2sq  14466  2sqlem7  14471