Theorem rexlimdv3a 2841

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

Syntax hints:   -> wi 4   /\ w3a 960   e. wcel 1761   E.wrex 2714

This theorem was proved from axioms:  ax-mp 5  ax-1 6  ax-2 7  ax-3 8  ax-gen 1596  ax-4 1607  ax-5 1675  ax-6 1713  ax-7 1733  ax-10 1780  ax-12 1797

This theorem depends on definitions:  df-bi 185  df-an 371  df-3an 962  df-ex 1592  df-nf 1595  df-ral 2718  df-rex 2719

This theorem is referenced by:  sorpssuni  6368  sorpssint  6369  tcrank  8087  rpnnen1lem5  10979  hashfun  12195  resqrex  12736  resqrcl  12739  lbsextlem3  17219  cmpsublem  18961  cmpcld  18964  ovoliunlem2  20945  isblo3i  24136  trisegint  27988  itg2addnclem  28368  areacirclem2  28410  rpnnen3lem  29305  dvconstbi  29533  expgrowth  29534  stoweidlem57  29777  sigarcol  29825  scmatsubcl  30767  scmatmulcl  30769  lshpnelb  32351  lsatfixedN  32376  lsmsatcv  32377  lssatomic  32378  lcv1  32408  lsatcvatlem  32416  islshpcv  32420  lfl1  32437  lshpsmreu  32476  lshpkrex  32485  lshpset2N  32486  lkrlspeqN  32538  cvrval3  32779  1cvratlt  32840  ps-2b  32848  llnnleat  32879  lvolex3N  32904  lplncvrlvol2  32981  osumcllem7N  33328  lhp0lt  33369  lhpj1  33388  4atexlemex6  33440  4atexlem7  33441  trlnidat  33539  cdlemd9  33572  cdleme21h  33700  cdlemg7fvbwN  33973  cdlemg7aN  33991  cdlemg34  34078  cdlemg36  34080  cdlemg44  34099  cdlemg48  34103  tendo1ne0  34194  cdlemk26-3  34272  cdlemk55b  34326  cdleml4N  34345  dih1dimatlem0  34695  dihglblem6  34707  dochshpncl  34751  dvh4dimlem  34810  dvh3dim2  34815  dvh3dim3N  34816  dochsatshpb  34819  dochexmidlem4  34830  dochexmidlem5  34831  dochexmidlem8  34834  dochkr1  34845  dochkr1OLDN  34846  lcfl7lem  34866  lcfl6  34867  lcfl8  34869  lcfrlem16  34925  lcfrlem40  34949  mapdval2N  34997  mapdrvallem2  35012  mapdpglem24  35071  mapdh6iN  35111  mapdh8ad  35146  mapdh8e  35151  hdmap1l6i  35186  hdmapval0  35203  hdmapevec  35205  hdmapval3N  35208  hdmap10lem  35209  hdmap11lem2  35212  hdmaprnlem15N  35231  hdmaprnlem16N  35232  hdmap14lem10  35247  hdmap14lem11  35248  hdmap14lem12  35249  hdmap14lem14  35251  hgmapval0  35262  hgmapval1  35263  hgmapadd  35264  hgmapmul  35265  hgmaprnlem3N  35268  hgmaprnlem4N  35269  hgmap11  35272  hgmapvvlem3  35295