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  6160  f1o2ndf1  6380  eroveu  6781  eroprf  6783  genipv  7707  genpelvl  7710  genpelvu  7711  genprndl  7719  genprndu  7720  addlocpr  7734  addnqprlemrl  7755  addnqprlemru  7756  mulnqprlemrl  7771  mulnqprlemru  7772  ltsopr  7794  ltaddpr  7795  ltexprlemfl  7807  ltexprlemrl  7808  ltexprlemfu  7809  ltexprlemru  7810  cauappcvgprlemladdfu  7852  cauappcvgprlemladdfl  7853  caucvgprlemdisj  7872  caucvgprlemladdfu  7875  caucvgprprlemdisj  7900  apreap  8745  apreim  8761  apirr  8763  apsym  8764  apcotr  8765  apadd1  8766  apneg  8769  mulext1  8770  apti  8780  aprcl  8804  qapne  9846  qtri3or  10472  exbtwnzlemex  10481  rebtwn2z  10486  cjap  11432  rexanre  11746  climcn2  11835  summodc  11909  prodmodclem2  12103  prodmodc  12104  eirrap  12304  dvds2lem  12329  bezoutlemnewy  12532  bezoutlembi  12541  dvdsmulgcd  12561  divgcdcoprm0  12638  cncongr1  12640  sqrt2irrap  12717  pcqmul  12841  pcneg  12863  pcadd  12878  4sqlem1  12926  4sqlem2  12927  4sqlem4  12930  mul4sq  12932  4sqlem12  12940  4sqlem13m  12941  4sqlem18  12946  imasaddfnlemg  13362  imasmnd2  13500  imasgrp2  13662  imasrng  13934  imasring  14042  dvdsrtr  14080  isnzr2  14163  lss1d  14362  znidom  14636  restbasg  14857  txbas  14947  blin2  15121  xmettxlem  15198  xmettx  15199  addcncntoplem  15250  mulcncf  15297  plyf  15426  plyadd  15440  plymul  15441  plyco  15448  plycj  15450  plycn  15451  plyrecj  15452  dvply2g  15455  logbgcd1irr  15656  logbgcd1irrap  15659  2sqlem5  15813  2sqlem9  15818  upgrpredgv  15959  usgredg4  16028