Theorem rexlimdvva 2496

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

Syntax hints:   -> wi 4   /\ wa 102   e. wcel 1438   E.wrex 2360

This theorem was proved from axioms:  ax-1 5  ax-2 6  ax-mp 7  ax-ia1 104  ax-ia2 105  ax-ia3 106  ax-5 1381  ax-gen 1383  ax-ie1 1427  ax-ie2 1428  ax-4 1445  ax-17 1464  ax-ial 1472  ax-i5r 1473

This theorem depends on definitions:  df-bi 115  df-nf 1395  df-ral 2364  df-rex 2365

This theorem is referenced by:  ovelrn  5793  f1o2ndf1  5993  eroveu  6381  eroprf  6383  genipv  7066  genpelvl  7069  genpelvu  7070  genprndl  7078  genprndu  7079  addlocpr  7093  addnqprlemrl  7114  addnqprlemru  7115  mulnqprlemrl  7130  mulnqprlemru  7131  ltsopr  7153  ltaddpr  7154  ltexprlemfl  7166  ltexprlemrl  7167  ltexprlemfu  7168  ltexprlemru  7169  cauappcvgprlemladdfu  7211  cauappcvgprlemladdfl  7212  caucvgprlemdisj  7231  caucvgprlemladdfu  7234  caucvgprprlemdisj  7259  apreap  8062  apreim  8078  apirr  8080  apsym  8081  apcotr  8082  apadd1  8083  apneg  8086  mulext1  8087  apti  8097  qapne  9122  qtri3or  9650  exbtwnzlemex  9657  rebtwn2z  9662  cjap  10336  rexanre  10649  climcn2  10694  isummo  10769  eirrap  11061  dvds2lem  11082  bezoutlemnewy  11259  bezoutlembi  11268  dvdsmulgcd  11288  divgcdcoprm0  11357  cncongr1  11359  sqrt2irrap  11432