Theorem rexlimivv 2617

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 2611	. 2 |- ( x e. A -> ( E. y e. B ph -> ps ) )
3	2	rexlimiv 2605	1 |- ( E. x e. A E. y e. B ph -> ps )

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:  opelxp  4690  f1o2ndf1  6283  xpdom2  6887  distrlem5prl  7648  distrlem5pru  7649  mulrid  8018  cnegex  8199  recexap  8674  creur  8980  creui  8981  cju  8982  elz2  9391  qre  9693  qaddcl  9703  qnegcl  9704  qmulcl  9705  qreccl  9710  elpqb  9718  replim  11006  prodmodc  11724  odd2np1  12017  opoe  12039  omoe  12040  opeo  12041  omeo  12042  qredeu  12238  pythagtriplem1  12406  pcz  12473  4sqlem1  12529  4sqlem2  12530  4sqlem4  12533  mul4sq  12535  txuni2  14435  blssioo  14732  tgioo  14733  elply  14913  2sqlem2  15272  mul2sq  15273  2sqlem7  15278