Theorem rexlimdvva 2633

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 2632	1 |- ( ph -> ( E. x e. A E. y e. B ps -> ch ) )

Syntax hints:   -> wi 4   /\ wa 104   e. wcel 2178   E.wrex 2487

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 1471  ax-gen 1473  ax-ie1 1517  ax-ie2 1518  ax-4 1534  ax-17 1550  ax-ial 1558  ax-i5r 1559

This theorem depends on definitions:  df-bi 117  df-nf 1485  df-ral 2491  df-rex 2492

This theorem is referenced by:  ovelrn  6118  f1o2ndf1  6337  eroveu  6736  eroprf  6738  genipv  7657  genpelvl  7660  genpelvu  7661  genprndl  7669  genprndu  7670  addlocpr  7684  addnqprlemrl  7705  addnqprlemru  7706  mulnqprlemrl  7721  mulnqprlemru  7722  ltsopr  7744  ltaddpr  7745  ltexprlemfl  7757  ltexprlemrl  7758  ltexprlemfu  7759  ltexprlemru  7760  cauappcvgprlemladdfu  7802  cauappcvgprlemladdfl  7803  caucvgprlemdisj  7822  caucvgprlemladdfu  7825  caucvgprprlemdisj  7850  apreap  8695  apreim  8711  apirr  8713  apsym  8714  apcotr  8715  apadd1  8716  apneg  8719  mulext1  8720  apti  8730  aprcl  8754  qapne  9795  qtri3or  10420  exbtwnzlemex  10429  rebtwn2z  10434  cjap  11332  rexanre  11646  climcn2  11735  summodc  11809  prodmodclem2  12003  prodmodc  12004  eirrap  12204  dvds2lem  12229  bezoutlemnewy  12432  bezoutlembi  12441  dvdsmulgcd  12461  divgcdcoprm0  12538  cncongr1  12540  sqrt2irrap  12617  pcqmul  12741  pcneg  12763  pcadd  12778  4sqlem1  12826  4sqlem2  12827  4sqlem4  12830  mul4sq  12832  4sqlem12  12840  4sqlem13m  12841  4sqlem18  12846  imasaddfnlemg  13261  imasmnd2  13399  imasgrp2  13561  imasrng  13833  imasring  13941  dvdsrtr  13978  isnzr2  14061  lss1d  14260  znidom  14534  restbasg  14755  txbas  14845  blin2  15019  xmettxlem  15096  xmettx  15097  addcncntoplem  15148  mulcncf  15195  plyf  15324  plyadd  15338  plymul  15339  plyco  15346  plycj  15348  plycn  15349  plyrecj  15350  dvply2g  15353  logbgcd1irr  15554  logbgcd1irrap  15557  2sqlem5  15711  2sqlem9  15716  upgrpredgv  15850