Theorem rexlimivv 2580

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

Syntax hints:   -> wi 4   /\ wa 103   e. wcel 2128   E.wrex 2436

This theorem was proved from axioms:  ax-mp 5  ax-1 6  ax-2 7  ax-ia1 105  ax-ia2 106  ax-ia3 107  ax-5 1427  ax-gen 1429  ax-ie1 1473  ax-ie2 1474  ax-4 1490  ax-17 1506  ax-ial 1514  ax-i5r 1515

This theorem depends on definitions:  df-bi 116  df-nf 1441  df-ral 2440  df-rex 2441

This theorem is referenced by:  opelxp  4617  f1o2ndf1  6176  xpdom2  6777  distrlem5prl  7507  distrlem5pru  7508  mulid1  7876  cnegex  8054  recexap  8528  creur  8831  creui  8832  cju  8833  elz2  9236  qre  9535  qaddcl  9545  qnegcl  9546  qmulcl  9547  qreccl  9552  elpqb  9559  replim  10763  prodmodc  11479  odd2np1  11768  opoe  11790  omoe  11791  opeo  11792  omeo  11793  qredeu  11978  pythagtriplem1  12144  txuni2  12698  blssioo  12987  tgioo  12988