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

Theorem sstr 3188
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 3187 . 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 3153
This theorem is referenced by:  sstrd  3190  sylan9ss  3193  ssdifss  3308  uneqin  3421  ssrnres  5115  relrelss  5194  fco  5363  fssres  5373  ssimaex  5545  dff3  5634  tpostpos2  6216  smores  6364  om00  6568  omeulem2  6576  pmss12g  6789  unblem1  7104  unblem2  7105  unblem3  7106  unblem4  7107  isfinite2  7110  cantnfval2  7365  cantnfle  7367  rankxplim3  7546  alephinit  7717  dfac12lem2  7765  ackbij1lem11  7851  cfeq0  7877  cfsuc  7878  cff1  7879  cflim2  7884  cfss  7886  cfslb2n  7889  cofsmo  7890  cfsmolem  7891  fin23lem34  7967  fin1a2lem13  8033  axdc3lem2  8072  axdclem  8141  pwcfsdom  8200  wunfi  8338  tskxpss  8389  tskcard  8398  suprzcl  10086  uzwo  10276  uzwoOLD  10277  uzwo2  10278  infmssuzle  10295  infmssuzcl  10296  supxrbnd  10641  supxrgtmnf  10642  supxrre1  10643  supxrre2  10644  supxrss  10645  iccsupr  10730  hashf1lem2  11388  fsum2d  12228  fsumabs  12253  fsumrlim  12263  fsumo1  12264  rpnnen2lem4  12490  rpnnen2lem7  12493  ramub2  13055  ressinbas  13198  ressress  13199  submre  13501  mrcss  13512  mreacs  13554  drsdirfi  14066  clatglbss  14225  ipopos  14257  cntz2ss  14802  ablfac1eulem  15301  subrgint  15561  tgval  16687  unitg  16699  mretopd  16823  ssnei  16841  opnneiss  16849  restdis  16903  restcls  16905  restntr  16906  tgcnp  16977  fbssfi  17526  fgss2  17563  fgcl  17567  supfil  17584  alexsubALTlem3  17737  alexsubALTlem4  17738  blssex  17967  mopni3  18034  metss  18048  metcnp3  18080  tgioo  18296  xrsmopn  18312  fsumcn  18368  cncfmptid  18410  iscmet3lem2  18712  caussi  18717  ovolsslem  18837  ovolsscl  18839  ovolssnul  18840  opnmblALT  18952  itgfsum  19175  limcresi  19229  dvmptfsum  19316  plyss  19575  chsupunss  21915  shsupunss  21917  spanss  21919  shslubi  21956  shlub  21985  mdsl1i  22893  mdsl2i  22894  cvmdi  22896  mdslmd1lem1  22897  mdslmd1lem2  22898  mdslmd2i  22902  mdslmd4i  22905  atomli  22954  atcvatlem  22957  chirredlem2  22963  chirredi  22966  mdsymlem5  22979  ballotlem2  23040  cvmlift2lem12  23249  inttrp  24506  int2pre  24636  fisub  24953  cmptdst  24967  limptlimpr2lem2  24974  islimrs4  24981  hdrmp  25105  dmrngcmp  25150  prismorcsetlemc  25316  lemindclsbu  25394  iscol3  25493  opnbnd  25642  fneint  25676  filbcmb  25831  lpss2  25867  heiborlem10  25943  igenmin  26088  isnacs3  26184  itgoss  26767  itgsinexplem1  27147  itgsinexp  27148  stoweidlem34  27182  stoweidlem57  27205  stoweidlem59  27207  sspwimp  27962  sspwimpVD  27963  lssatle  28472  paddss1  29273  paddss2  29274  paddss12  29275  paddssw2  29300  pclssN  29350  pclfinN  29356  polsubN  29363  2polvalN  29370  2polssN  29371  3polN  29372  2pmaplubN  29382  pnonsingN  29389  polsubclN  29408  dihord6apre  30713  dochsscl  30825  mapdordlem2  31094
This theorem was proved from axioms:  ax-1 7  ax-2 8  ax-3 9  ax-mp 10  ax-gen 1534  ax-5 1545  ax-17 1604  ax-9 1637  ax-8 1645  ax-6 1704  ax-7 1709  ax-11 1716  ax-12 1867  ax-ext 2265
This theorem depends on definitions:  df-bi 179  df-an 362  df-tru 1312  df-ex 1530  df-nf 1533  df-sb 1632  df-clab 2271  df-cleq 2277  df-clel 2280  df-in 3160  df-ss 3167
  Copyright terms: Public domain W3C validator