Theorem rexlimdvva 2560

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

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

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 1424  ax-gen 1426  ax-ie1 1470  ax-ie2 1471  ax-4 1488  ax-17 1507  ax-ial 1515  ax-i5r 1516

This theorem depends on definitions:  df-bi 116  df-nf 1438  df-ral 2422  df-rex 2423

This theorem is referenced by:  ovelrn  5927  f1o2ndf1  6133  eroveu  6528  eroprf  6530  genipv  7341  genpelvl  7344  genpelvu  7345  genprndl  7353  genprndu  7354  addlocpr  7368  addnqprlemrl  7389  addnqprlemru  7390  mulnqprlemrl  7405  mulnqprlemru  7406  ltsopr  7428  ltaddpr  7429  ltexprlemfl  7441  ltexprlemrl  7442  ltexprlemfu  7443  ltexprlemru  7444  cauappcvgprlemladdfu  7486  cauappcvgprlemladdfl  7487  caucvgprlemdisj  7506  caucvgprlemladdfu  7509  caucvgprprlemdisj  7534  apreap  8373  apreim  8389  apirr  8391  apsym  8392  apcotr  8393  apadd1  8394  apneg  8397  mulext1  8398  apti  8408  aprcl  8432  qapne  9458  qtri3or  10051  exbtwnzlemex  10058  rebtwn2z  10063  cjap  10710  rexanre  11024  climcn2  11110  summodc  11184  prodmodclem2  11378  prodmodc  11379  eirrap  11520  dvds2lem  11541  bezoutlemnewy  11720  bezoutlembi  11729  dvdsmulgcd  11749  divgcdcoprm0  11818  cncongr1  11820  sqrt2irrap  11894  restbasg  12376  txbas  12466  blin2  12640  xmettxlem  12717  xmettx  12718  addcncntoplem  12759  mulcncf  12799  logbgcd1irr  13092  logbgcd1irrap  13095