Theorem rexlimdv3a 2926

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

Syntax hints:   -> wi 4   /\ w3a 982   e. wcel 1870   E.wrex 2783

This theorem was proved from axioms:  ax-mp 5  ax-1 6  ax-2 7  ax-3 8  ax-gen 1665  ax-4 1678  ax-5 1751

This theorem depends on definitions:  df-bi 188  df-an 372  df-3an 984  df-ex 1660  df-ral 2787  df-rex 2788

This theorem is referenced by:  sorpssuni  6594  sorpssint  6595  tcrank  8354  rpnnen1lem5  11294  hashfun  12604  resqrex  13293  resqrtcl  13296  prmgaplem6  14989  lbsextlem3  18318  cmpsublem  20345  cmpcld  20348  ovoliunlem2  22334  isblo3i  26287  trisegint  30580  itg2addnclem  31700  areacirclem2  31740  lshpnelb  32262  lsatfixedN  32287  lsmsatcv  32288  lssatomic  32289  lcv1  32319  lsatcvatlem  32327  islshpcv  32331  lfl1  32348  lshpsmreu  32387  lshpkrex  32396  lshpset2N  32397  lkrlspeqN  32449  cvrval3  32690  1cvratlt  32751  ps-2b  32759  llnnleat  32790  lvolex3N  32815  lplncvrlvol2  32892  osumcllem7N  33239  lhp0lt  33280  lhpj1  33299  4atexlemex6  33351  4atexlem7  33352  trlnidat  33451  cdlemd9  33484  cdleme21h  33613  cdlemg7fvbwN  33886  cdlemg7aN  33904  cdlemg34  33991  cdlemg36  33993  cdlemg44  34012  cdlemg48  34016  tendo1ne0  34107  cdlemk26-3  34185  cdlemk55b  34239  cdleml4N  34258  dih1dimatlem0  34608  dihglblem6  34620  dochshpncl  34664  dvh4dimlem  34723  dvh3dim2  34728  dvh3dim3N  34729  dochsatshpb  34732  dochexmidlem4  34743  dochexmidlem5  34744  dochexmidlem8  34747  dochkr1  34758  dochkr1OLDN  34759  lcfl7lem  34779  lcfl6  34780  lcfl8  34782  lcfrlem16  34838  lcfrlem40  34862  mapdval2N  34910  mapdrvallem2  34925  mapdpglem24  34984  mapdh6iN  35024  mapdh8ad  35059  mapdh8e  35064  hdmap1l6i  35099  hdmapval0  35116  hdmapevec  35118  hdmapval3N  35121  hdmap10lem  35122  hdmap11lem2  35125  hdmaprnlem15N  35144  hdmaprnlem16N  35145  hdmap14lem10  35160  hdmap14lem11  35161  hdmap14lem12  35162  hdmap14lem14  35164  hgmapval0  35175  hgmapval1  35176  hgmapadd  35177  hgmapmul  35178  hgmaprnlem3N  35181  hgmaprnlem4N  35182  hgmap11  35185  hgmapvvlem3  35208  rpnnen3lem  35595  dvconstbi  36323  expgrowth  36324  limccog  37275  0ellimcdiv  37305  cosknegpi  37319  cncfshift  37326  cncfperiod  37331  cncfuni  37339  icccncfext  37340  dvbdfbdioolem1  37375  itgperiod  37430  stoweidlem57  37490  fourierdlem12  37553  fourierdlem48  37589  fourierdlem49  37590  fourierdlem52  37593  fourierdlem54  37595  fourierdlem68  37609  fourierdlem77  37618  fourierdlem83  37624  fourierdlem87  37628  fourierdlem102  37643  fourierdlem103  37644  fourierdlem104  37645  fourierdlem113  37654  fourierdlem114  37655  etransclem24  37693  etransclem32  37701  etransclem48  37717  sigarcol  37876