Theorem rexlimdv3a 2864

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

Syntax hints:   -> wi 4   /\ w3a 965   e. wcel 1756   E.wrex 2737

This theorem was proved from axioms:  ax-mp 5  ax-1 6  ax-2 7  ax-3 8  ax-gen 1591  ax-4 1602  ax-5 1670  ax-6 1708  ax-7 1728  ax-10 1775  ax-12 1792

This theorem depends on definitions:  df-bi 185  df-an 371  df-3an 967  df-ex 1587  df-nf 1590  df-ral 2741  df-rex 2742

This theorem is referenced by:  sorpssuni  6390  sorpssint  6391  tcrank  8112  rpnnen1lem5  11004  hashfun  12220  resqrex  12761  resqrcl  12764  lbsextlem3  17263  cmpsublem  19024  cmpcld  19027  ovoliunlem2  21008  isblo3i  24223  trisegint  28081  itg2addnclem  28469  areacirclem2  28511  rpnnen3lem  29406  dvconstbi  29634  expgrowth  29635  stoweidlem57  29878  sigarcol  29926  scmatsubcl  30923  scmatmulcl  30925  lshpnelb  32725  lsatfixedN  32750  lsmsatcv  32751  lssatomic  32752  lcv1  32782  lsatcvatlem  32790  islshpcv  32794  lfl1  32811  lshpsmreu  32850  lshpkrex  32859  lshpset2N  32860  lkrlspeqN  32912  cvrval3  33153  1cvratlt  33214  ps-2b  33222  llnnleat  33253  lvolex3N  33278  lplncvrlvol2  33355  osumcllem7N  33702  lhp0lt  33743  lhpj1  33762  4atexlemex6  33814  4atexlem7  33815  trlnidat  33913  cdlemd9  33946  cdleme21h  34074  cdlemg7fvbwN  34347  cdlemg7aN  34365  cdlemg34  34452  cdlemg36  34454  cdlemg44  34473  cdlemg48  34477  tendo1ne0  34568  cdlemk26-3  34646  cdlemk55b  34700  cdleml4N  34719  dih1dimatlem0  35069  dihglblem6  35081  dochshpncl  35125  dvh4dimlem  35184  dvh3dim2  35189  dvh3dim3N  35190  dochsatshpb  35193  dochexmidlem4  35204  dochexmidlem5  35205  dochexmidlem8  35208  dochkr1  35219  dochkr1OLDN  35220  lcfl7lem  35240  lcfl6  35241  lcfl8  35243  lcfrlem16  35299  lcfrlem40  35323  mapdval2N  35371  mapdrvallem2  35386  mapdpglem24  35445  mapdh6iN  35485  mapdh8ad  35520  mapdh8e  35525  hdmap1l6i  35560  hdmapval0  35577  hdmapevec  35579  hdmapval3N  35582  hdmap10lem  35583  hdmap11lem2  35586  hdmaprnlem15N  35605  hdmaprnlem16N  35606  hdmap14lem10  35621  hdmap14lem11  35622  hdmap14lem12  35623  hdmap14lem14  35625  hgmapval0  35636  hgmapval1  35637  hgmapadd  35638  hgmapmul  35639  hgmaprnlem3N  35642  hgmaprnlem4N  35643  hgmap11  35646  hgmapvvlem3  35669