Theorem rexlimdv3a 2852

Description: Inference from Theorem 19.23 of [Margaris] p. 90 (restricted quantifier version). Frequently-used variant of rexlimdv 2848. (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 1204	. 2 |- ( ph -> ( x e. A -> ( ps -> ch ) ) )
3	2	rexlimdv 2848	1 |- ( ph -> ( E. x e. A ps -> ch ) )

Syntax hints:   -> wi 4   /\ w3a 982   e. wcel 1872   E.wrex 2709

This theorem was proved from axioms:  ax-mp 5  ax-1 6  ax-2 7  ax-3 8  ax-gen 1663  ax-4 1676  ax-5 1752

This theorem depends on definitions:  df-bi 188  df-an 372  df-3an 984  df-ex 1658  df-ral 2713  df-rex 2714

This theorem is referenced by:  sorpssuni  6531  sorpssint  6532  tcrank  8300  rpnnen1lem5  11238  hashfun  12550  resqrex  13251  resqrtcl  13254  prmgaplem6  14962  lbsextlem3  18319  cmpsublem  20349  cmpcld  20352  ovoliunlem2  22391  isblo3i  26377  trisegint  30737  itg2addnclem  31894  areacirclem2  31934  lshpnelb  32456  lsatfixedN  32481  lsmsatcv  32482  lssatomic  32483  lcv1  32513  lsatcvatlem  32521  islshpcv  32525  lfl1  32542  lshpsmreu  32581  lshpkrex  32590  lshpset2N  32591  lkrlspeqN  32643  cvrval3  32884  1cvratlt  32945  ps-2b  32953  llnnleat  32984  lvolex3N  33009  lplncvrlvol2  33086  osumcllem7N  33433  lhp0lt  33474  lhpj1  33493  4atexlemex6  33545  4atexlem7  33546  trlnidat  33645  cdlemd9  33678  cdleme21h  33807  cdlemg7fvbwN  34080  cdlemg7aN  34098  cdlemg34  34185  cdlemg36  34187  cdlemg44  34206  cdlemg48  34210  tendo1ne0  34301  cdlemk26-3  34379  cdlemk55b  34433  cdleml4N  34452  dih1dimatlem0  34802  dihglblem6  34814  dochshpncl  34858  dvh4dimlem  34917  dvh3dim2  34922  dvh3dim3N  34923  dochsatshpb  34926  dochexmidlem4  34937  dochexmidlem5  34938  dochexmidlem8  34941  dochkr1  34952  dochkr1OLDN  34953  lcfl7lem  34973  lcfl6  34974  lcfl8  34976  lcfrlem16  35032  lcfrlem40  35056  mapdval2N  35104  mapdrvallem2  35119  mapdpglem24  35178  mapdh6iN  35218  mapdh8ad  35253  mapdh8e  35258  hdmap1l6i  35293  hdmapval0  35310  hdmapevec  35312  hdmapval3N  35315  hdmap10lem  35316  hdmap11lem2  35319  hdmaprnlem15N  35338  hdmaprnlem16N  35339  hdmap14lem10  35354  hdmap14lem11  35355  hdmap14lem12  35356  hdmap14lem14  35358  hgmapval0  35369  hgmapval1  35370  hgmapadd  35371  hgmapmul  35372  hgmaprnlem3N  35375  hgmaprnlem4N  35376  hgmap11  35379  hgmapvvlem3  35402  rpnnen3lem  35793  dvconstbi  36590  expgrowth  36591  limccog  37577  0ellimcdiv  37607  cosknegpi  37621  cncfshift  37628  cncfperiod  37633  cncfuni  37641  icccncfext  37642  dvbdfbdioolem1  37677  itgperiod  37735  stoweidlem57  37795  fourierdlem12  37858  fourierdlem48  37895  fourierdlem49  37896  fourierdlem52  37899  fourierdlem54  37901  fourierdlem68  37915  fourierdlem77  37924  fourierdlem83  37930  fourierdlem87  37934  fourierdlem102  37949  fourierdlem103  37950  fourierdlem104  37951  fourierdlem113  37960  fourierdlem114  37961  elaa2  37976  etransclem24  38000  etransclem32  38008  etransclem48OLD  38024  etransclem48  38025  sigarcol  38281