Theorem rexlimdv3a 2957

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

Syntax hints:   -> wi 4   /\ w3a 973   e. wcel 1767   E.wrex 2815

This theorem was proved from axioms:  ax-mp 5  ax-1 6  ax-2 7  ax-3 8  ax-gen 1601  ax-4 1612  ax-5 1680

This theorem depends on definitions:  df-bi 185  df-an 371  df-3an 975  df-ex 1597  df-ral 2819  df-rex 2820

This theorem is referenced by:  sorpssuni  6574  sorpssint  6575  tcrank  8303  rpnnen1lem5  11213  hashfun  12462  resqrex  13050  resqrtcl  13053  lbsextlem3  17618  cmpsublem  19705  cmpcld  19708  ovoliunlem2  21741  isblo3i  25489  trisegint  29531  itg2addnclem  29919  areacirclem2  29961  rpnnen3lem  30804  dvconstbi  31066  expgrowth  31067  stoweidlem57  31584  fourierdlem12  31646  sigarcol  31775  lshpnelb  33998  lsatfixedN  34023  lsmsatcv  34024  lssatomic  34025  lcv1  34055  lsatcvatlem  34063  islshpcv  34067  lfl1  34084  lshpsmreu  34123  lshpkrex  34132  lshpset2N  34133  lkrlspeqN  34185  cvrval3  34426  1cvratlt  34487  ps-2b  34495  llnnleat  34526  lvolex3N  34551  lplncvrlvol2  34628  osumcllem7N  34975  lhp0lt  35016  lhpj1  35035  4atexlemex6  35087  4atexlem7  35088  trlnidat  35186  cdlemd9  35219  cdleme21h  35347  cdlemg7fvbwN  35620  cdlemg7aN  35638  cdlemg34  35725  cdlemg36  35727  cdlemg44  35746  cdlemg48  35750  tendo1ne0  35841  cdlemk26-3  35919  cdlemk55b  35973  cdleml4N  35992  dih1dimatlem0  36342  dihglblem6  36354  dochshpncl  36398  dvh4dimlem  36457  dvh3dim2  36462  dvh3dim3N  36463  dochsatshpb  36466  dochexmidlem4  36477  dochexmidlem5  36478  dochexmidlem8  36481  dochkr1  36492  dochkr1OLDN  36493  lcfl7lem  36513  lcfl6  36514  lcfl8  36516  lcfrlem16  36572  lcfrlem40  36596  mapdval2N  36644  mapdrvallem2  36659  mapdpglem24  36718  mapdh6iN  36758  mapdh8ad  36793  mapdh8e  36798  hdmap1l6i  36833  hdmapval0  36850  hdmapevec  36852  hdmapval3N  36855  hdmap10lem  36856  hdmap11lem2  36859  hdmaprnlem15N  36878  hdmaprnlem16N  36879  hdmap14lem10  36894  hdmap14lem11  36895  hdmap14lem12  36896  hdmap14lem14  36898  hgmapval0  36909  hgmapval1  36910  hgmapadd  36911  hgmapmul  36912  hgmaprnlem3N  36915  hgmaprnlem4N  36916  hgmap11  36919  hgmapvvlem3  36942