MPE Home Metamath Proof Explorer < Previous   Next >
Nearby theorems
Mirrors  >  Home  >  MPE Home  >  Th. List  >  rexlimdv3a Unicode version

Theorem rexlimdv3a 2669
Description: Inference from Theorem 19.23 of [Margaris] p. 90 (restricted quantifier version). Frequently-used variant of rexlimdv 2666. (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
StepHypRef Expression
1 rexlimdv3a.1 . . 3  |-  ( (
ph  /\  x  e.  A  /\  ps )  ->  ch )
213exp 1150 . 2  |-  ( ph  ->  ( x  e.  A  ->  ( ps  ->  ch ) ) )
32rexlimdv 2666 1  |-  ( ph  ->  ( E. x  e.  A  ps  ->  ch ) )
Colors of variables: wff set class
Syntax hints:    -> wi 4    /\ w3a 934    e. wcel 1684   E.wrex 2544
This theorem is referenced by:  sorpssuni  6286  sorpssint  6287  tcrank  7554  rpnnen1lem5  10346  hashfun  11389  resqrex  11736  resqrcl  11739  lbsextlem3  15913  cmpsublem  17126  cmpcld  17129  ovoliunlem2  18862  isblo3i  21379  trisegint  24651  areacirclem4  24927  rpnnen3lem  27124  dvconstbi  27551  expgrowth  27552  sigarcol  27854  lshpnelb  29174  lsatfixedN  29199  lsmsatcv  29200  lssatomic  29201  lcv1  29231  lsatcvatlem  29239  islshpcv  29243  lfl1  29260  lshpsmreu  29299  lshpkrex  29308  lshpset2N  29309  lkrlspeqN  29361  cvrval3  29602  1cvratlt  29663  ps-2b  29671  llnnleat  29702  lvolex3N  29727  lplncvrlvol2  29804  osumcllem7N  30151  lhp0lt  30192  lhpj1  30211  4atexlemex6  30263  4atexlem7  30264  trlnidat  30362  cdlemd9  30395  cdleme21h  30523  cdlemg7fvbwN  30796  cdlemg7aN  30814  cdlemg34  30901  cdlemg36  30903  cdlemg44  30922  cdlemg48  30926  tendo1ne0  31017  cdlemk26-3  31095  cdlemk55b  31149  cdleml4N  31168  dih1dimatlem0  31518  dihglblem6  31530  dochshpncl  31574  dvh4dimlem  31633  dvh3dim2  31638  dvh3dim3N  31639  dochsatshpb  31642  dochexmidlem4  31653  dochexmidlem5  31654  dochexmidlem8  31657  dochkr1  31668  dochkr1OLDN  31669  lcfl7lem  31689  lcfl6  31690  lcfl8  31692  lcfrlem16  31748  lcfrlem40  31772  mapdval2N  31820  mapdrvallem2  31835  mapdpglem24  31894  mapdh6iN  31934  mapdh8ad  31969  mapdh8e  31974  hdmap1l6i  32009  hdmapval0  32026  hdmapevec  32028  hdmapval3N  32031  hdmap10lem  32032  hdmap11lem2  32035  hdmaprnlem15N  32054  hdmaprnlem16N  32055  hdmap14lem10  32070  hdmap14lem11  32071  hdmap14lem12  32072  hdmap14lem14  32074  hgmapval0  32085  hgmapval1  32086  hgmapadd  32087  hgmapmul  32088  hgmaprnlem3N  32091  hgmaprnlem4N  32092  hgmap11  32095  hgmapvvlem3  32118
This theorem was proved from axioms:  ax-1 5  ax-2 6  ax-3 7  ax-mp 8  ax-gen 1533  ax-5 1544  ax-17 1603  ax-9 1635  ax-8 1643  ax-6 1703  ax-11 1715
This theorem depends on definitions:  df-bi 177  df-an 360  df-3an 936  df-ex 1529  df-nf 1532  df-ral 2548  df-rex 2549
  Copyright terms: Public domain W3C validator