Theorem rexlimdv3a 2892

Description: Inference from Theorem 19.23 of [Margaris] p. 90 (restricted quantifier version). Frequently-used variant of rexlimdv 2888. (Contributed by NM, 7-Jun-2015.)

Hypothesis

Ref	Expression
rexlimdv3a.1	|- ( ( ph /\ x e. A /\ ps ) -> ch )

Assertion

Ref	Expression
rexlimdv3a	|- ( ph -> ( E. x e. A ps -> ch ) )

Distinct variable groups:   ph, x   ch, x

Allowed substitution hints:   ps( x)   A( x)

Proof of Theorem rexlimdv3a

Step	Hyp	Ref	Expression
1		rexlimdv3a.1	. . 3 |- ( ( ph /\ x e. A /\ ps ) -> ch )
2	1	3exp 1214	. 2 |- ( ph -> ( x e. A -> ( ps -> ch ) ) )
3	2	rexlimdv 2888	1 |- ( ph -> ( E. x e. A ps -> ch ) )

Syntax hints:   -> wi 4   /\ w3a 991   e. wcel 1897   E.wrex 2749

This theorem was proved from axioms:  ax-mp 5  ax-1 6  ax-2 7  ax-3 8  ax-gen 1679  ax-4 1692  ax-5 1768

This theorem depends on definitions:  df-bi 190  df-an 377  df-3an 993  df-ex 1674  df-ral 2753  df-rex 2754

This theorem is referenced by:  sorpssuni  6606  sorpssint  6607  tcrank  8380  rpnnen1lem5  11322  hashfun  12641  resqrex  13362  resqrtcl  13365  prmgaplem6  15074  lbsextlem3  18431  cmpsublem  20462  cmpcld  20465  ovoliunlem2  22504  isblo3i  26490  trisegint  30843  itg2addnclem  32037  areacirclem2  32077  lshpnelb  32594  lsatfixedN  32619  lsmsatcv  32620  lssatomic  32621  lcv1  32651  lsatcvatlem  32659  islshpcv  32663  lfl1  32680  lshpsmreu  32719  lshpkrex  32728  lshpset2N  32729  lkrlspeqN  32781  cvrval3  33022  1cvratlt  33083  ps-2b  33091  llnnleat  33122  lvolex3N  33147  lplncvrlvol2  33224  osumcllem7N  33571  lhp0lt  33612  lhpj1  33631  4atexlemex6  33683  4atexlem7  33684  trlnidat  33783  cdlemd9  33816  cdleme21h  33945  cdlemg7fvbwN  34218  cdlemg7aN  34236  cdlemg34  34323  cdlemg36  34325  cdlemg44  34344  cdlemg48  34348  tendo1ne0  34439  cdlemk26-3  34517  cdlemk55b  34571  cdleml4N  34590  dih1dimatlem0  34940  dihglblem6  34952  dochshpncl  34996  dvh4dimlem  35055  dvh3dim2  35060  dvh3dim3N  35061  dochsatshpb  35064  dochexmidlem4  35075  dochexmidlem5  35076  dochexmidlem8  35079  dochkr1  35090  dochkr1OLDN  35091  lcfl7lem  35111  lcfl6  35112  lcfl8  35114  lcfrlem16  35170  lcfrlem40  35194  mapdval2N  35242  mapdrvallem2  35257  mapdpglem24  35316  mapdh6iN  35356  mapdh8ad  35391  mapdh8e  35396  hdmap1l6i  35431  hdmapval0  35448  hdmapevec  35450  hdmapval3N  35453  hdmap10lem  35454  hdmap11lem2  35457  hdmaprnlem15N  35476  hdmaprnlem16N  35477  hdmap14lem10  35492  hdmap14lem11  35493  hdmap14lem12  35494  hdmap14lem14  35496  hgmapval0  35507  hgmapval1  35508  hgmapadd  35509  hgmapmul  35510  hgmaprnlem3N  35513  hgmaprnlem4N  35514  hgmap11  35517  hgmapvvlem3  35540  rpnnen3lem  35930  dvconstbi  36726  expgrowth  36727  limccog  37737  0ellimcdiv  37767  cosknegpi  37781  cncfshift  37788  cncfperiod  37793  cncfuni  37801  icccncfext  37802  dvbdfbdioolem1  37837  itgperiod  37895  stoweidlem57  37955  fourierdlem12  38018  fourierdlem48  38055  fourierdlem49  38056  fourierdlem52  38059  fourierdlem54  38061  fourierdlem68  38075  fourierdlem77  38084  fourierdlem83  38090  fourierdlem87  38094  fourierdlem102  38109  fourierdlem103  38110  fourierdlem104  38111  fourierdlem113  38120  fourierdlem114  38121  elaa2  38136  etransclem24  38160  etransclem32  38168  etransclem48OLD  38184  etransclem48  38185  sigarcol  38510