Theorem rexlimdvva 2656

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

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

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 1493  ax-gen 1495  ax-ie1 1539  ax-ie2 1540  ax-4 1556  ax-17 1572  ax-ial 1580  ax-i5r 1581

This theorem depends on definitions:  df-bi 117  df-nf 1507  df-ral 2513  df-rex 2514

This theorem is referenced by:  ovelrn  6166  f1o2ndf1  6388  eroveu  6790  eroprf  6792  genipv  7719  genpelvl  7722  genpelvu  7723  genprndl  7731  genprndu  7732  addlocpr  7746  addnqprlemrl  7767  addnqprlemru  7768  mulnqprlemrl  7783  mulnqprlemru  7784  ltsopr  7806  ltaddpr  7807  ltexprlemfl  7819  ltexprlemrl  7820  ltexprlemfu  7821  ltexprlemru  7822  cauappcvgprlemladdfu  7864  cauappcvgprlemladdfl  7865  caucvgprlemdisj  7884  caucvgprlemladdfu  7887  caucvgprprlemdisj  7912  apreap  8757  apreim  8773  apirr  8775  apsym  8776  apcotr  8777  apadd1  8778  apneg  8781  mulext1  8782  apti  8792  aprcl  8816  qapne  9863  qtri3or  10490  exbtwnzlemex  10499  rebtwn2z  10504  cjap  11457  rexanre  11771  climcn2  11860  summodc  11934  prodmodclem2  12128  prodmodc  12129  eirrap  12329  dvds2lem  12354  bezoutlemnewy  12557  bezoutlembi  12566  dvdsmulgcd  12586  divgcdcoprm0  12663  cncongr1  12665  sqrt2irrap  12742  pcqmul  12866  pcneg  12888  pcadd  12903  4sqlem1  12951  4sqlem2  12952  4sqlem4  12955  mul4sq  12957  4sqlem12  12965  4sqlem13m  12966  4sqlem18  12971  imasaddfnlemg  13387  imasmnd2  13525  imasgrp2  13687  imasrng  13959  imasring  14067  dvdsrtr  14105  isnzr2  14188  lss1d  14387  znidom  14661  restbasg  14882  txbas  14972  blin2  15146  xmettxlem  15223  xmettx  15224  addcncntoplem  15275  mulcncf  15322  plyf  15451  plyadd  15465  plymul  15466  plyco  15473  plycj  15475  plycn  15476  plyrecj  15477  dvply2g  15480  logbgcd1irr  15681  logbgcd1irrap  15684  2sqlem5  15838  2sqlem9  15843  upgrpredgv  15985  usgredg4  16054  usgr1vr  16087