Theorem rexlimdvva 2590

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 114	. 2 |- ( ph -> ( ( x e. A /\ y e. B ) -> ( ps -> ch ) ) )
3	2	rexlimdvv 2589	1 |- ( ph -> ( E. x e. A E. y e. B ps -> ch ) )

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

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 1435  ax-gen 1437  ax-ie1 1481  ax-ie2 1482  ax-4 1498  ax-17 1514  ax-ial 1522  ax-i5r 1523

This theorem depends on definitions:  df-bi 116  df-nf 1449  df-ral 2448  df-rex 2449

This theorem is referenced by:  ovelrn  5986  f1o2ndf1  6192  eroveu  6588  eroprf  6590  genipv  7446  genpelvl  7449  genpelvu  7450  genprndl  7458  genprndu  7459  addlocpr  7473  addnqprlemrl  7494  addnqprlemru  7495  mulnqprlemrl  7510  mulnqprlemru  7511  ltsopr  7533  ltaddpr  7534  ltexprlemfl  7546  ltexprlemrl  7547  ltexprlemfu  7548  ltexprlemru  7549  cauappcvgprlemladdfu  7591  cauappcvgprlemladdfl  7592  caucvgprlemdisj  7611  caucvgprlemladdfu  7614  caucvgprprlemdisj  7639  apreap  8481  apreim  8497  apirr  8499  apsym  8500  apcotr  8501  apadd1  8502  apneg  8505  mulext1  8506  apti  8516  aprcl  8540  qapne  9573  qtri3or  10174  exbtwnzlemex  10181  rebtwn2z  10186  cjap  10844  rexanre  11158  climcn2  11246  summodc  11320  prodmodclem2  11514  prodmodc  11515  eirrap  11714  dvds2lem  11739  bezoutlemnewy  11925  bezoutlembi  11934  dvdsmulgcd  11954  divgcdcoprm0  12029  cncongr1  12031  sqrt2irrap  12108  pcqmul  12231  pcneg  12252  pcadd  12267  4sqlem1  12314  4sqlem2  12315  4sqlem4  12318  mul4sq  12320  restbasg  12768  txbas  12858  blin2  13032  xmettxlem  13109  xmettx  13110  addcncntoplem  13151  mulcncf  13191  logbgcd1irr  13485  logbgcd1irrap  13488  2sqlem5  13555  2sqlem9  13560