Theorem rexlimdvva 2602

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

Syntax hints:   -> wi 4   /\ wa 104   e. wcel 2148   E.wrex 2456

This theorem was proved from axioms:  ax-mp 5  ax-1 6  ax-2 7  ax-ia1 106  ax-ia2 107  ax-ia3 108  ax-5 1447  ax-gen 1449  ax-ie1 1493  ax-ie2 1494  ax-4 1510  ax-17 1526  ax-ial 1534  ax-i5r 1535

This theorem depends on definitions:  df-bi 117  df-nf 1461  df-ral 2460  df-rex 2461

This theorem is referenced by:  ovelrn  6022  f1o2ndf1  6228  eroveu  6625  eroprf  6627  genipv  7507  genpelvl  7510  genpelvu  7511  genprndl  7519  genprndu  7520  addlocpr  7534  addnqprlemrl  7555  addnqprlemru  7556  mulnqprlemrl  7571  mulnqprlemru  7572  ltsopr  7594  ltaddpr  7595  ltexprlemfl  7607  ltexprlemrl  7608  ltexprlemfu  7609  ltexprlemru  7610  cauappcvgprlemladdfu  7652  cauappcvgprlemladdfl  7653  caucvgprlemdisj  7672  caucvgprlemladdfu  7675  caucvgprprlemdisj  7700  apreap  8543  apreim  8559  apirr  8561  apsym  8562  apcotr  8563  apadd1  8564  apneg  8567  mulext1  8568  apti  8578  aprcl  8602  qapne  9638  qtri3or  10242  exbtwnzlemex  10249  rebtwn2z  10254  cjap  10914  rexanre  11228  climcn2  11316  summodc  11390  prodmodclem2  11584  prodmodc  11585  eirrap  11784  dvds2lem  11809  bezoutlemnewy  11996  bezoutlembi  12005  dvdsmulgcd  12025  divgcdcoprm0  12100  cncongr1  12102  sqrt2irrap  12179  pcqmul  12302  pcneg  12323  pcadd  12338  4sqlem1  12385  4sqlem2  12386  4sqlem4  12389  mul4sq  12391  imasaddfnlemg  12734  dvdsrtr  13268  restbasg  13638  txbas  13728  blin2  13902  xmettxlem  13979  xmettx  13980  addcncntoplem  14021  mulcncf  14061  logbgcd1irr  14355  logbgcd1irrap  14358  2sqlem5  14436  2sqlem9  14441