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

Theorem sstr 3187
Description: Transitivity of subclasses. Theorem 6 of [Suppes] p. 23. (Contributed by NM, 5-Sep-2003.)
Assertion
Ref Expression
sstr  |-  ( ( A  C_  B  /\  B  C_  C )  ->  A  C_  C )

Proof of Theorem sstr
StepHypRef Expression
1 sstr2 3186 . 2  |-  ( A 
C_  B  ->  ( B  C_  C  ->  A  C_  C ) )
21imp 418 1  |-  ( ( A  C_  B  /\  B  C_  C )  ->  A  C_  C )
Colors of variables: wff set class
Syntax hints:    -> wi 4    /\ wa 358    C_ wss 3152
This theorem is referenced by:  sstrd  3189  sylan9ss  3192  ssdifss  3307  uneqin  3420  ssrnres  5116  relrelss  5196  fco  5398  fssres  5408  ssimaex  5584  dff3  5673  tpostpos2  6255  smores  6369  om00  6573  omeulem2  6581  pmss12g  6794  unblem1  7109  unblem2  7110  unblem3  7111  unblem4  7112  isfinite2  7115  cantnfval2  7370  cantnfle  7372  rankxplim3  7551  alephinit  7722  dfac12lem2  7770  ackbij1lem11  7856  cfeq0  7882  cfsuc  7883  cff1  7884  cflim2  7889  cfss  7891  cfslb2n  7894  cofsmo  7895  cfsmolem  7896  fin23lem34  7972  fin1a2lem13  8038  axdc3lem2  8077  axdclem  8146  pwcfsdom  8205  wunfi  8343  tskxpss  8394  tskcard  8403  suprzcl  10091  uzwo  10281  uzwoOLD  10282  uzwo2  10283  infmssuzle  10300  infmssuzcl  10301  supxrbnd  10647  supxrgtmnf  10648  supxrre1  10649  supxrre2  10650  supxrss  10651  iccsupr  10736  hashf1lem2  11394  fsum2d  12234  fsumabs  12259  fsumrlim  12269  fsumo1  12270  rpnnen2lem4  12496  rpnnen2lem7  12499  ramub2  13061  ressinbas  13204  ressress  13205  submre  13507  mrcss  13518  mreacs  13560  drsdirfi  14072  clatglbss  14231  ipopos  14263  cntz2ss  14808  ablfac1eulem  15307  subrgint  15567  tgval  16693  unitg  16705  mretopd  16829  ssnei  16847  opnneiss  16855  restdis  16909  restcls  16911  restntr  16912  tgcnp  16983  fbssfi  17532  fgss2  17569  fgcl  17573  supfil  17590  alexsubALTlem3  17743  alexsubALTlem4  17744  blssex  17973  mopni3  18040  metss  18054  metcnp3  18086  tgioo  18302  xrsmopn  18318  fsumcn  18374  cncfmptid  18416  iscmet3lem2  18718  caussi  18723  ovolsslem  18843  ovolsscl  18845  ovolssnul  18846  opnmblALT  18958  itgfsum  19181  limcresi  19235  dvmptfsum  19322  plyss  19581  chsupunss  21923  shsupunss  21925  spanss  21927  shslubi  21964  shlub  21993  mdsl1i  22901  mdsl2i  22902  cvmdi  22904  mdslmd1lem1  22905  mdslmd1lem2  22906  mdslmd2i  22910  mdslmd4i  22913  atomli  22962  atcvatlem  22965  chirredlem2  22971  chirredi  22974  mdsymlem5  22987  ballotlem2  23047  tpr2rico  23296  sigainb  23497  insiga  23498  cvmlift2lem12  23845  inttrp  25108  int2pre  25237  fisub  25554  cmptdst  25568  limptlimpr2lem2  25575  islimrs4  25582  hdrmp  25706  dmrngcmp  25751  prismorcsetlemc  25917  lemindclsbu  25995  iscol3  26094  opnbnd  26243  fneint  26277  filbcmb  26432  lpss2  26468  heiborlem10  26544  igenmin  26689  isnacs3  26785  itgoss  27368  itgsinexplem1  27748  itgsinexp  27749  stoweidlem34  27783  stoweidlem57  27806  stoweidlem59  27808  sspwimp  28694  sspwimpVD  28695  lssatle  29205  paddss1  30006  paddss2  30007  paddss12  30008  paddssw2  30033  pclssN  30083  pclfinN  30089  polsubN  30096  2polvalN  30103  2polssN  30104  3polN  30105  2pmaplubN  30115  pnonsingN  30122  polsubclN  30141  dihord6apre  31446  dochsscl  31558  mapdordlem2  31827
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-7 1708  ax-11 1715  ax-12 1866  ax-ext 2264
This theorem depends on definitions:  df-bi 177  df-an 360  df-tru 1310  df-ex 1529  df-nf 1532  df-sb 1630  df-clab 2270  df-cleq 2276  df-clel 2279  df-in 3159  df-ss 3166
  Copyright terms: Public domain W3C validator