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  6026  f1o2ndf1  6232  eroveu  6629  eroprf  6631  genipv  7511  genpelvl  7514  genpelvu  7515  genprndl  7523  genprndu  7524  addlocpr  7538  addnqprlemrl  7559  addnqprlemru  7560  mulnqprlemrl  7575  mulnqprlemru  7576  ltsopr  7598  ltaddpr  7599  ltexprlemfl  7611  ltexprlemrl  7612  ltexprlemfu  7613  ltexprlemru  7614  cauappcvgprlemladdfu  7656  cauappcvgprlemladdfl  7657  caucvgprlemdisj  7676  caucvgprlemladdfu  7679  caucvgprprlemdisj  7704  apreap  8547  apreim  8563  apirr  8565  apsym  8566  apcotr  8567  apadd1  8568  apneg  8571  mulext1  8572  apti  8582  aprcl  8606  qapne  9642  qtri3or  10246  exbtwnzlemex  10253  rebtwn2z  10258  cjap  10918  rexanre  11232  climcn2  11320  summodc  11394  prodmodclem2  11588  prodmodc  11589  eirrap  11788  dvds2lem  11813  bezoutlemnewy  12000  bezoutlembi  12009  dvdsmulgcd  12029  divgcdcoprm0  12104  cncongr1  12106  sqrt2irrap  12183  pcqmul  12306  pcneg  12327  pcadd  12342  4sqlem1  12389  4sqlem2  12390  4sqlem4  12393  mul4sq  12395  imasaddfnlemg  12741  dvdsrtr  13276  lss1d  13476  restbasg  13808  txbas  13898  blin2  14072  xmettxlem  14149  xmettx  14150  addcncntoplem  14191  mulcncf  14231  logbgcd1irr  14525  logbgcd1irrap  14528  2sqlem5  14606  2sqlem9  14611