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

Theorem sstr 3108
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 3107 . 2  |-  ( A 
C_  B  ->  ( B  C_  C  ->  A  C_  C ) )
21imp 420 1  |-  ( ( A  C_  B  /\  B  C_  C )  ->  A  C_  C )
Colors of variables: wff set class
Syntax hints:    -> wi 6    /\ wa 360    C_ wss 3078
This theorem is referenced by:  sstrd  3110  sylan9ss  3113  ssdifss  3221  uneqin  3327  ssrnres  5023  relrelss  5102  fco  5255  fssres  5265  ssimaex  5436  dff3  5525  tpostpos2  6107  smores  6255  om00  6459  omeulem2  6467  pmss12g  6680  unblem1  6994  unblem2  6995  unblem3  6996  unblem4  6997  isfinite2  7000  cantnfval2  7254  cantnfle  7256  rankxplim3  7435  alephinit  7606  dfac12lem2  7654  ackbij1lem11  7740  cfeq0  7766  cfsuc  7767  cff1  7768  cflim2  7773  cfss  7775  cfslb2n  7778  cofsmo  7779  cfsmolem  7780  fin23lem34  7856  fin1a2lem13  7922  axdc3lem2  7961  axdclem  8030  pwcfsdom  8085  wunfi  8223  tskxpss  8274  tskcard  8283  suprzcl  9970  uzwo  10160  uzwoOLD  10161  uzwo2  10162  infmssuzle  10179  infmssuzcl  10180  supxrbnd  10525  supxrgtmnf  10526  supxrre1  10527  supxrre2  10528  supxrss  10529  iccsupr  10614  hashf1lem2  11271  fsum2d  12111  fsumabs  12136  fsumrlim  12146  fsumo1  12147  rpnnen2lem4  12370  rpnnen2lem7  12373  ramub2  12935  ressinbas  13078  ressress  13079  submre  13379  mrcss  13390  mreacs  13404  drsdirfi  13916  clatglbss  14075  ipopos  14107  cntz2ss  14643  ablfac1eulem  15142  subrgint  15402  tgval  16525  unitg  16537  mretopd  16661  ssnei  16679  opnneiss  16687  restdis  16741  restcls  16743  restntr  16744  tgcnp  16815  fbssfi  17364  fgss2  17401  fgcl  17405  supfil  17422  alexsubALTlem3  17575  alexsubALTlem4  17576  blssex  17805  mopni3  17872  metss  17886  metcnp3  17918  tgioo  18134  xrsmopn  18150  fsumcn  18206  cncfmptid  18248  iscmet3lem2  18550  caussi  18555  ovolsslem  18675  ovolsscl  18677  ovolssnul  18678  opnmblALT  18790  itgfsum  19013  limcresi  19067  dvmptfsum  19154  plyss  19413  chsupunss  21753  shsupunss  21755  spanss  21757  shslubi  21794  shlub  21823  mdsl1i  22731  mdsl2i  22732  cvmdi  22734  mdslmd1lem1  22735  mdslmd1lem2  22736  mdslmd2i  22740  mdslmd4i  22743  atomli  22792  atcvatlem  22795  chirredlem2  22801  chirredi  22804  mdsymlem5  22817  cvmlift2lem12  23016  inttrp  24273  int2pre  24403  fisub  24720  cmptdst  24734  limptlimpr2lem2  24741  islimrs4  24748  hdrmp  24872  dmrngcmp  24917  prismorcsetlemc  25083  lemindclsbu  25161  iscol3  25260  opnbnd  25409  fneint  25443  filbcmb  25598  lpss2  25634  heiborlem10  25710  igenmin  25855  isnacs3  25951  itgoss  26534  stoweidlem34  26917  stoweidlem57  26940  stoweidlem59  26942  sspwimp  27481  sspwimpVD  27482  lssatle  28109  paddss1  28910  paddss2  28911  paddss12  28912  paddssw2  28937  pclssN  28987  pclfinN  28993  polsubN  29000  2polvalN  29007  2polssN  29008  3polN  29009  2pmaplubN  29019  pnonsingN  29026  polsubclN  29045  dihord6apre  30350  dochsscl  30462  mapdordlem2  30731
This theorem was proved from axioms:  ax-1 7  ax-2 8  ax-3 9  ax-mp 10  ax-5 1533  ax-6 1534  ax-7 1535  ax-gen 1536  ax-8 1623  ax-11 1624  ax-17 1628  ax-12o 1664  ax-10 1678  ax-9 1684  ax-4 1692  ax-16 1926  ax-ext 2234
This theorem depends on definitions:  df-bi 179  df-an 362  df-tru 1315  df-ex 1538  df-nf 1540  df-sb 1883  df-clab 2240  df-cleq 2246  df-clel 2249  df-in 3085  df-ss 3089
  Copyright terms: Public domain W3C validator