Theorem rexlimdvva 2602

Description: Inference from Theorem 19.23 of [Margaris] p. 90. (Restricted quantifier version.) (Contributed by NM, 18-Jun-2014.)

Hypothesis

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

Assertion

Ref	Expression
rexlimdvva	|- ( 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 rexlimdvva

Step	Hyp	Ref	Expression
1		rexlimdvva.1	. . 3 |- ( ( ph /\ ( x e. A /\ y e. B ) ) -> ( ps -> ch ) )
2	1	ex 115	. 2 |- ( ph -> ( ( x e. A /\ y e. B ) -> ( ps -> ch ) ) )
3	2	rexlimdvv 2601	1 |- ( ph -> ( E. x e. A E. y e. B ps -> ch ) )

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:  ovelrn  6018  f1o2ndf1  6224  eroveu  6621  eroprf  6623  genipv  7503  genpelvl  7506  genpelvu  7507  genprndl  7515  genprndu  7516  addlocpr  7530  addnqprlemrl  7551  addnqprlemru  7552  mulnqprlemrl  7567  mulnqprlemru  7568  ltsopr  7590  ltaddpr  7591  ltexprlemfl  7603  ltexprlemrl  7604  ltexprlemfu  7605  ltexprlemru  7606  cauappcvgprlemladdfu  7648  cauappcvgprlemladdfl  7649  caucvgprlemdisj  7668  caucvgprlemladdfu  7671  caucvgprprlemdisj  7696  apreap  8538  apreim  8554  apirr  8556  apsym  8557  apcotr  8558  apadd1  8559  apneg  8562  mulext1  8563  apti  8573  aprcl  8597  qapne  9633  qtri3or  10236  exbtwnzlemex  10243  rebtwn2z  10248  cjap  10906  rexanre  11220  climcn2  11308  summodc  11382  prodmodclem2  11576  prodmodc  11577  eirrap  11776  dvds2lem  11801  bezoutlemnewy  11987  bezoutlembi  11996  dvdsmulgcd  12016  divgcdcoprm0  12091  cncongr1  12093  sqrt2irrap  12170  pcqmul  12293  pcneg  12314  pcadd  12329  4sqlem1  12376  4sqlem2  12377  4sqlem4  12380  mul4sq  12382  dvdsrtr  13169  restbasg  13450  txbas  13540  blin2  13714  xmettxlem  13791  xmettx  13792  addcncntoplem  13833  mulcncf  13873  logbgcd1irr  14167  logbgcd1irrap  14170  2sqlem5  14237  2sqlem9  14242