Theorem rexlimdvva 2631

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

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

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 1470  ax-gen 1472  ax-ie1 1516  ax-ie2 1517  ax-4 1533  ax-17 1549  ax-ial 1557  ax-i5r 1558

This theorem depends on definitions:  df-bi 117  df-nf 1484  df-ral 2489  df-rex 2490

This theorem is referenced by:  ovelrn  6095  f1o2ndf1  6314  eroveu  6713  eroprf  6715  genipv  7622  genpelvl  7625  genpelvu  7626  genprndl  7634  genprndu  7635  addlocpr  7649  addnqprlemrl  7670  addnqprlemru  7671  mulnqprlemrl  7686  mulnqprlemru  7687  ltsopr  7709  ltaddpr  7710  ltexprlemfl  7722  ltexprlemrl  7723  ltexprlemfu  7724  ltexprlemru  7725  cauappcvgprlemladdfu  7767  cauappcvgprlemladdfl  7768  caucvgprlemdisj  7787  caucvgprlemladdfu  7790  caucvgprprlemdisj  7815  apreap  8660  apreim  8676  apirr  8678  apsym  8679  apcotr  8680  apadd1  8681  apneg  8684  mulext1  8685  apti  8695  aprcl  8719  qapne  9760  qtri3or  10383  exbtwnzlemex  10392  rebtwn2z  10397  cjap  11217  rexanre  11531  climcn2  11620  summodc  11694  prodmodclem2  11888  prodmodc  11889  eirrap  12089  dvds2lem  12114  bezoutlemnewy  12317  bezoutlembi  12326  dvdsmulgcd  12346  divgcdcoprm0  12423  cncongr1  12425  sqrt2irrap  12502  pcqmul  12626  pcneg  12648  pcadd  12663  4sqlem1  12711  4sqlem2  12712  4sqlem4  12715  mul4sq  12717  4sqlem12  12725  4sqlem13m  12726  4sqlem18  12731  imasaddfnlemg  13146  imasmnd2  13284  imasgrp2  13446  imasrng  13718  imasring  13826  dvdsrtr  13863  isnzr2  13946  lss1d  14145  znidom  14419  restbasg  14640  txbas  14730  blin2  14904  xmettxlem  14981  xmettx  14982  addcncntoplem  15033  mulcncf  15080  plyf  15209  plyadd  15223  plymul  15224  plyco  15231  plycj  15233  plycn  15234  plyrecj  15235  dvply2g  15238  logbgcd1irr  15439  logbgcd1irrap  15442  2sqlem5  15596  2sqlem9  15601