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  6025  f1o2ndf1  6231  eroveu  6628  eroprf  6630  genipv  7510  genpelvl  7513  genpelvu  7514  genprndl  7522  genprndu  7523  addlocpr  7537  addnqprlemrl  7558  addnqprlemru  7559  mulnqprlemrl  7574  mulnqprlemru  7575  ltsopr  7597  ltaddpr  7598  ltexprlemfl  7610  ltexprlemrl  7611  ltexprlemfu  7612  ltexprlemru  7613  cauappcvgprlemladdfu  7655  cauappcvgprlemladdfl  7656  caucvgprlemdisj  7675  caucvgprlemladdfu  7678  caucvgprprlemdisj  7703  apreap  8546  apreim  8562  apirr  8564  apsym  8565  apcotr  8566  apadd1  8567  apneg  8570  mulext1  8571  apti  8581  aprcl  8605  qapne  9641  qtri3or  10245  exbtwnzlemex  10252  rebtwn2z  10257  cjap  10917  rexanre  11231  climcn2  11319  summodc  11393  prodmodclem2  11587  prodmodc  11588  eirrap  11787  dvds2lem  11812  bezoutlemnewy  11999  bezoutlembi  12008  dvdsmulgcd  12028  divgcdcoprm0  12103  cncongr1  12105  sqrt2irrap  12182  pcqmul  12305  pcneg  12326  pcadd  12341  4sqlem1  12388  4sqlem2  12389  4sqlem4  12392  mul4sq  12394  imasaddfnlemg  12740  dvdsrtr  13275  lss1d  13475  restbasg  13707  txbas  13797  blin2  13971  xmettxlem  14048  xmettx  14049  addcncntoplem  14090  mulcncf  14130  logbgcd1irr  14424  logbgcd1irrap  14427  2sqlem5  14505  2sqlem9  14510