Theorem rexlimdvva 2434

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

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

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 1333  ax-gen 1335  ax-ie1 1379  ax-ie2 1380  ax-4 1397  ax-17 1416  ax-ial 1424  ax-i5r 1425

This theorem depends on definitions:  df-bi 110  df-nf 1347  df-ral 2305  df-rex 2306

This theorem is referenced by:  ovelrn  5591  f1o2ndf1  5791  eroveu  6133  eroprf  6135  genipv  6492  genpelvl  6495  genpelvu  6496  genprndl  6504  genprndu  6505  addlocpr  6519  addnqprlemrl  6538  addnqprlemru  6539  ltsopr  6570  ltaddpr  6571  ltexprlemfl  6583  ltexprlemrl  6584  ltexprlemfu  6585  ltexprlemru  6586  cauappcvgprlemladdfu  6626  cauappcvgprlemladdfl  6627  caucvgprlemdisj  6645  caucvgprlemladdfu  6648  apreap  7371  apreim  7387  apirr  7389  apsym  7390  apcotr  7391  apadd1  7392  apneg  7395  mulext1  7396  apti  7406  qapne  8350  cjap  9134