Theorem rexlimdvva 2630

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

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

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 1469  ax-gen 1471  ax-ie1 1515  ax-ie2 1516  ax-4 1532  ax-17 1548  ax-ial 1556  ax-i5r 1557

This theorem depends on definitions:  df-bi 117  df-nf 1483  df-ral 2488  df-rex 2489

This theorem is referenced by:  ovelrn  6094  f1o2ndf1  6313  eroveu  6712  eroprf  6714  genipv  7621  genpelvl  7624  genpelvu  7625  genprndl  7633  genprndu  7634  addlocpr  7648  addnqprlemrl  7669  addnqprlemru  7670  mulnqprlemrl  7685  mulnqprlemru  7686  ltsopr  7708  ltaddpr  7709  ltexprlemfl  7721  ltexprlemrl  7722  ltexprlemfu  7723  ltexprlemru  7724  cauappcvgprlemladdfu  7766  cauappcvgprlemladdfl  7767  caucvgprlemdisj  7786  caucvgprlemladdfu  7789  caucvgprprlemdisj  7814  apreap  8659  apreim  8675  apirr  8677  apsym  8678  apcotr  8679  apadd1  8680  apneg  8683  mulext1  8684  apti  8694  aprcl  8718  qapne  9759  qtri3or  10381  exbtwnzlemex  10390  rebtwn2z  10395  cjap  11188  rexanre  11502  climcn2  11591  summodc  11665  prodmodclem2  11859  prodmodc  11860  eirrap  12060  dvds2lem  12085  bezoutlemnewy  12288  bezoutlembi  12297  dvdsmulgcd  12317  divgcdcoprm0  12394  cncongr1  12396  sqrt2irrap  12473  pcqmul  12597  pcneg  12619  pcadd  12634  4sqlem1  12682  4sqlem2  12683  4sqlem4  12686  mul4sq  12688  4sqlem12  12696  4sqlem13m  12697  4sqlem18  12702  imasaddfnlemg  13117  imasmnd2  13255  imasgrp2  13417  imasrng  13689  imasring  13797  dvdsrtr  13834  isnzr2  13917  lss1d  14116  znidom  14390  restbasg  14611  txbas  14701  blin2  14875  xmettxlem  14952  xmettx  14953  addcncntoplem  15004  mulcncf  15051  plyf  15180  plyadd  15194  plymul  15195  plyco  15202  plycj  15204  plycn  15205  plyrecj  15206  dvply2g  15209  logbgcd1irr  15410  logbgcd1irrap  15413  2sqlem5  15567  2sqlem9  15572