Theorem rexlimdv3a 2948

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

Syntax hints:   -> wi 4   /\ w3a 971   e. wcel 1823   E.wrex 2805

This theorem was proved from axioms:  ax-mp 5  ax-1 6  ax-2 7  ax-3 8  ax-gen 1623  ax-4 1636  ax-5 1709

This theorem depends on definitions:  df-bi 185  df-an 369  df-3an 973  df-ex 1618  df-ral 2809  df-rex 2810

This theorem is referenced by:  sorpssuni  6562  sorpssint  6563  tcrank  8293  rpnnen1lem5  11213  hashfun  12479  resqrex  13166  resqrtcl  13169  lbsextlem3  18001  cmpsublem  20066  cmpcld  20069  ovoliunlem2  22080  isblo3i  25914  trisegint  29906  itg2addnclem  30306  areacirclem2  30348  rpnnen3lem  31212  dvconstbi  31480  expgrowth  31481  limccog  31865  0ellimcdiv  31894  cosknegpi  31908  cncfshift  31915  cncfperiod  31920  cncfuni  31928  icccncfext  31929  dvbdfbdioolem1  31964  itgperiod  32019  stoweidlem57  32078  fourierdlem12  32140  fourierdlem48  32176  fourierdlem49  32177  fourierdlem52  32180  fourierdlem54  32182  fourierdlem68  32196  fourierdlem77  32205  fourierdlem83  32211  fourierdlem87  32215  fourierdlem102  32230  fourierdlem103  32231  fourierdlem104  32232  fourierdlem113  32241  fourierdlem114  32242  etransclem24  32280  etransclem32  32288  etransclem48  32304  sigarcol  32320  lshpnelb  35106  lsatfixedN  35131  lsmsatcv  35132  lssatomic  35133  lcv1  35163  lsatcvatlem  35171  islshpcv  35175  lfl1  35192  lshpsmreu  35231  lshpkrex  35240  lshpset2N  35241  lkrlspeqN  35293  cvrval3  35534  1cvratlt  35595  ps-2b  35603  llnnleat  35634  lvolex3N  35659  lplncvrlvol2  35736  osumcllem7N  36083  lhp0lt  36124  lhpj1  36143  4atexlemex6  36195  4atexlem7  36196  trlnidat  36295  cdlemd9  36328  cdleme21h  36457  cdlemg7fvbwN  36730  cdlemg7aN  36748  cdlemg34  36835  cdlemg36  36837  cdlemg44  36856  cdlemg48  36860  tendo1ne0  36951  cdlemk26-3  37029  cdlemk55b  37083  cdleml4N  37102  dih1dimatlem0  37452  dihglblem6  37464  dochshpncl  37508  dvh4dimlem  37567  dvh3dim2  37572  dvh3dim3N  37573  dochsatshpb  37576  dochexmidlem4  37587  dochexmidlem5  37588  dochexmidlem8  37591  dochkr1  37602  dochkr1OLDN  37603  lcfl7lem  37623  lcfl6  37624  lcfl8  37626  lcfrlem16  37682  lcfrlem40  37706  mapdval2N  37754  mapdrvallem2  37769  mapdpglem24  37828  mapdh6iN  37868  mapdh8ad  37903  mapdh8e  37908  hdmap1l6i  37943  hdmapval0  37960  hdmapevec  37962  hdmapval3N  37965  hdmap10lem  37966  hdmap11lem2  37969  hdmaprnlem15N  37988  hdmaprnlem16N  37989  hdmap14lem10  38004  hdmap14lem11  38005  hdmap14lem12  38006  hdmap14lem14  38008  hgmapval0  38019  hgmapval1  38020  hgmapadd  38021  hgmapmul  38022  hgmaprnlem3N  38025  hgmaprnlem4N  38026  hgmap11  38029  hgmapvvlem3  38052