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  4656  f1o2ndf1  6228  xpdom2  6830  distrlem5prl  7584  distrlem5pru  7585  mulrid  7953  cnegex  8134  recexap  8609  creur  8915  creui  8916  cju  8917  elz2  9323  qre  9624  qaddcl  9634  qnegcl  9635  qmulcl  9636  qreccl  9641  elpqb  9648  replim  10867  prodmodc  11585  odd2np1  11877  opoe  11899  omoe  11900  opeo  11901  omeo  11902  qredeu  12096  pythagtriplem1  12264  pcz  12330  4sqlem1  12385  4sqlem2  12386  4sqlem4  12389  mul4sq  12391  txuni2  13726  blssioo  14015  tgioo  14016  2sqlem2  14432  mul2sq  14433  2sqlem7  14438