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

Theorem rexlimdv3a 2670
Description: Inference from Theorem 19.23 of [Margaris] p. 90 (restricted quantifier version). Frequently-used variant of rexlimdv 2667. (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 2667 1  |-  ( ph  ->  ( E. x  e.  A  ps  ->  ch ) )
Colors of variables: wff set class
Syntax hints:    -> wi 4    /\ w3a 934    e. wcel 1685   E.wrex 2545
This theorem is referenced by:  sorpssuni  6248  sorpssint  6249  tcrank  7550  rpnnen1lem5  10342  hashfun  11385  resqrex  11732  resqrcl  11735  lbsextlem3  15909  cmpsublem  17122  cmpcld  17125  ovoliunlem2  18858  isblo3i  21373  trisegint  24061  areacirclem4  24337  rpnnen3lem  26535  dvconstbi  26962  expgrowth  26963  lshpnelb  28453  lsatfixedN  28478  lsmsatcv  28479  lssatomic  28480  lcv1  28510  lsatcvatlem  28518  islshpcv  28522  lfl1  28539  lshpsmreu  28578  lshpkrex  28587  lshpset2N  28588  lkrlspeqN  28640  cvrval3  28881  1cvratlt  28942  ps-2b  28950  llnnleat  28981  lvolex3N  29006  lplncvrlvol2  29083  osumcllem7N  29430  lhp0lt  29471  lhpj1  29490  4atexlemex6  29542  4atexlem7  29543  trlnidat  29641  cdlemd9  29674  cdleme21h  29802  cdlemg7fvbwN  30075  cdlemg7aN  30093  cdlemg34  30180  cdlemg36  30182  cdlemg44  30201  cdlemg48  30205  tendo1ne0  30296  cdlemk26-3  30374  cdlemk55b  30428  cdleml4N  30447  dih1dimatlem0  30797  dihglblem6  30809  dochshpncl  30853  dvh4dimlem  30912  dvh3dim2  30917  dvh3dim3N  30918  dochsatshpb  30921  dochexmidlem4  30932  dochexmidlem5  30933  dochexmidlem8  30936  dochkr1  30947  dochkr1OLDN  30948  lcfl7lem  30968  lcfl6  30969  lcfl8  30971  lcfrlem16  31027  lcfrlem40  31051  mapdval2N  31099  mapdrvallem2  31114  mapdpglem24  31173  mapdh6iN  31213  mapdh8ad  31248  mapdh8e  31253  hdmap1l6i  31288  hdmapval0  31305  hdmapevec  31307  hdmapval3N  31310  hdmap10lem  31311  hdmap11lem2  31314  hdmaprnlem15N  31333  hdmaprnlem16N  31334  hdmap14lem10  31349  hdmap14lem11  31350  hdmap14lem12  31351  hdmap14lem14  31353  hgmapval0  31364  hgmapval1  31365  hgmapadd  31366  hgmapmul  31367  hgmaprnlem3N  31370  hgmaprnlem4N  31371  hgmap11  31374  hgmapvvlem3  31397
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 1636  ax-8 1644  ax-6 1704  ax-11 1716
This theorem depends on definitions:  df-bi 177  df-an 360  df-3an 936  df-ex 1529  df-nf 1532  df-ral 2549  df-rex 2550
  Copyright terms: Public domain W3C validator