Theorem rexlimdvva 2555

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

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

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 1423  ax-gen 1425  ax-ie1 1469  ax-ie2 1470  ax-4 1487  ax-17 1506  ax-ial 1514  ax-i5r 1515

This theorem depends on definitions:  df-bi 116  df-nf 1437  df-ral 2419  df-rex 2420

This theorem is referenced by:  ovelrn  5912  f1o2ndf1  6118  eroveu  6513  eroprf  6515  genipv  7310  genpelvl  7313  genpelvu  7314  genprndl  7322  genprndu  7323  addlocpr  7337  addnqprlemrl  7358  addnqprlemru  7359  mulnqprlemrl  7374  mulnqprlemru  7375  ltsopr  7397  ltaddpr  7398  ltexprlemfl  7410  ltexprlemrl  7411  ltexprlemfu  7412  ltexprlemru  7413  cauappcvgprlemladdfu  7455  cauappcvgprlemladdfl  7456  caucvgprlemdisj  7475  caucvgprlemladdfu  7478  caucvgprprlemdisj  7503  apreap  8342  apreim  8358  apirr  8360  apsym  8361  apcotr  8362  apadd1  8363  apneg  8366  mulext1  8367  apti  8377  aprcl  8401  qapne  9424  qtri3or  10013  exbtwnzlemex  10020  rebtwn2z  10025  cjap  10671  rexanre  10985  climcn2  11071  summodc  11145  eirrap  11473  dvds2lem  11494  bezoutlemnewy  11673  bezoutlembi  11682  dvdsmulgcd  11702  divgcdcoprm0  11771  cncongr1  11773  sqrt2irrap  11847  restbasg  12326  txbas  12416  blin2  12590  xmettxlem  12667  xmettx  12668  addcncntoplem  12709  mulcncf  12749