Theorem rexlimdvva 2619

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

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

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 1458  ax-gen 1460  ax-ie1 1504  ax-ie2 1505  ax-4 1521  ax-17 1537  ax-ial 1545  ax-i5r 1546

This theorem depends on definitions:  df-bi 117  df-nf 1472  df-ral 2477  df-rex 2478

This theorem is referenced by:  ovelrn  6069  f1o2ndf1  6283  eroveu  6682  eroprf  6684  genipv  7571  genpelvl  7574  genpelvu  7575  genprndl  7583  genprndu  7584  addlocpr  7598  addnqprlemrl  7619  addnqprlemru  7620  mulnqprlemrl  7635  mulnqprlemru  7636  ltsopr  7658  ltaddpr  7659  ltexprlemfl  7671  ltexprlemrl  7672  ltexprlemfu  7673  ltexprlemru  7674  cauappcvgprlemladdfu  7716  cauappcvgprlemladdfl  7717  caucvgprlemdisj  7736  caucvgprlemladdfu  7739  caucvgprprlemdisj  7764  apreap  8608  apreim  8624  apirr  8626  apsym  8627  apcotr  8628  apadd1  8629  apneg  8632  mulext1  8633  apti  8643  aprcl  8667  qapne  9707  qtri3or  10313  exbtwnzlemex  10321  rebtwn2z  10326  cjap  11053  rexanre  11367  climcn2  11455  summodc  11529  prodmodclem2  11723  prodmodc  11724  eirrap  11924  dvds2lem  11949  bezoutlemnewy  12136  bezoutlembi  12145  dvdsmulgcd  12165  divgcdcoprm0  12242  cncongr1  12244  sqrt2irrap  12321  pcqmul  12444  pcneg  12466  pcadd  12481  4sqlem1  12529  4sqlem2  12530  4sqlem4  12533  mul4sq  12535  4sqlem12  12543  4sqlem13m  12544  4sqlem18  12549  imasaddfnlemg  12900  imasgrp2  13183  imasrng  13455  imasring  13563  dvdsrtr  13600  isnzr2  13683  lss1d  13882  znidom  14156  restbasg  14347  txbas  14437  blin2  14611  xmettxlem  14688  xmettx  14689  addcncntoplem  14740  mulcncf  14787  plyf  14916  plyadd  14930  plymul  14931  plyco  14937  plycj  14939  plycn  14940  plyrecj  14941  logbgcd1irr  15140  logbgcd1irrap  15143  2sqlem5  15276  2sqlem9  15281