Theorem rexlimdv3a 2792

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

Syntax hints:   -> wi 4   /\ w3a 936   e. wcel 1721   E.wrex 2667

This theorem is referenced by:  sorpssuni  6490  sorpssint  6491  tcrank  7764  rpnnen1lem5  10560  hashfun  11655  resqrex  12011  resqrcl  12014  lbsextlem3  16187  cmpsublem  17416  cmpcld  17419  ovoliunlem2  19352  isblo3i  22255  trisegint  25866  itg2addnclem  26155  areacirclem4  26183  rpnnen3lem  26992  dvconstbi  27419  expgrowth  27420  stoweidlem57  27673  sigarcol  27721  lshpnelb  29467  lsatfixedN  29492  lsmsatcv  29493  lssatomic  29494  lcv1  29524  lsatcvatlem  29532  islshpcv  29536  lfl1  29553  lshpsmreu  29592  lshpkrex  29601  lshpset2N  29602  lkrlspeqN  29654  cvrval3  29895  1cvratlt  29956  ps-2b  29964  llnnleat  29995  lvolex3N  30020  lplncvrlvol2  30097  osumcllem7N  30444  lhp0lt  30485  lhpj1  30504  4atexlemex6  30556  4atexlem7  30557  trlnidat  30655  cdlemd9  30688  cdleme21h  30816  cdlemg7fvbwN  31089  cdlemg7aN  31107  cdlemg34  31194  cdlemg36  31196  cdlemg44  31215  cdlemg48  31219  tendo1ne0  31310  cdlemk26-3  31388  cdlemk55b  31442  cdleml4N  31461  dih1dimatlem0  31811  dihglblem6  31823  dochshpncl  31867  dvh4dimlem  31926  dvh3dim2  31931  dvh3dim3N  31932  dochsatshpb  31935  dochexmidlem4  31946  dochexmidlem5  31947  dochexmidlem8  31950  dochkr1  31961  dochkr1OLDN  31962  lcfl7lem  31982  lcfl6  31983  lcfl8  31985  lcfrlem16  32041  lcfrlem40  32065  mapdval2N  32113  mapdrvallem2  32128  mapdpglem24  32187  mapdh6iN  32227  mapdh8ad  32262  mapdh8e  32267  hdmap1l6i  32302  hdmapval0  32319  hdmapevec  32321  hdmapval3N  32324  hdmap10lem  32325  hdmap11lem2  32328  hdmaprnlem15N  32347  hdmaprnlem16N  32348  hdmap14lem10  32363  hdmap14lem11  32364  hdmap14lem12  32365  hdmap14lem14  32367  hgmapval0  32378  hgmapval1  32379  hgmapadd  32380  hgmapmul  32381  hgmaprnlem3N  32384  hgmaprnlem4N  32385  hgmap11  32388  hgmapvvlem3  32411

This theorem was proved from axioms:  ax-1 5  ax-2 6  ax-3 7  ax-mp 8  ax-gen 1552  ax-5 1563  ax-17 1623  ax-9 1662  ax-8 1683  ax-6 1740  ax-11 1757

This theorem depends on definitions:  df-bi 178  df-an 361  df-3an 938  df-ex 1548  df-nf 1551  df-ral 2671  df-rex 2672