Theorem rexlimdvva 2440

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 108	. 2 |- ( ph -> ( ( x e. A /\ y e. B ) -> ( ps -> ch ) ) )
3	2	rexlimdvv 2439	1 |- ( ph -> ( E. x e. A E. y e. B ps -> ch ) )

Syntax hints:   -> wi 4   /\ wa 97   e. wcel 1393   E.wrex 2307

This theorem was proved from axioms:  ax-1 5  ax-2 6  ax-mp 7  ax-ia1 99  ax-ia2 100  ax-ia3 101  ax-5 1336  ax-gen 1338  ax-ie1 1382  ax-ie2 1383  ax-4 1400  ax-17 1419  ax-ial 1427  ax-i5r 1428

This theorem depends on definitions:  df-bi 110  df-nf 1350  df-ral 2311  df-rex 2312

This theorem is referenced by:  ovelrn  5649  f1o2ndf1  5849  eroveu  6197  eroprf  6199  genipv  6607  genpelvl  6610  genpelvu  6611  genprndl  6619  genprndu  6620  addlocpr  6634  addnqprlemrl  6655  addnqprlemru  6656  mulnqprlemrl  6671  mulnqprlemru  6672  ltsopr  6694  ltaddpr  6695  ltexprlemfl  6707  ltexprlemrl  6708  ltexprlemfu  6709  ltexprlemru  6710  cauappcvgprlemladdfu  6752  cauappcvgprlemladdfl  6753  caucvgprlemdisj  6772  caucvgprlemladdfu  6775  caucvgprprlemdisj  6800  apreap  7578  apreim  7594  apirr  7596  apsym  7597  apcotr  7598  apadd1  7599  apneg  7602  mulext1  7603  apti  7613  qapne  8574  qtri3or  9098  qbtwnzlemex  9105  rebtwn2z  9109  cjap  9506  climcn2  9830