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

Theorem sstr 3356
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 3355 . 2  |-  ( A 
C_  B  ->  ( B  C_  C  ->  A  C_  C ) )
21imp 419 1  |-  ( ( A  C_  B  /\  B  C_  C )  ->  A  C_  C )
Colors of variables: wff set class
Syntax hints:    -> wi 4    /\ wa 359    C_ wss 3320
This theorem is referenced by:  sstrd  3358  sylan9ss  3361  ssdifss  3478  uneqin  3592  ssrnres  5309  relrelss  5393  fco  5600  fssres  5610  ssimaex  5788  dff3  5882  tpostpos2  6500  smores  6614  om00  6818  omeulem2  6826  pmss12g  7040  unblem1  7359  unblem2  7360  unblem3  7361  unblem4  7362  isfinite2  7365  cantnfval2  7624  cantnfle  7626  rankxplim3  7805  alephinit  7976  dfac12lem2  8024  ackbij1lem11  8110  cfeq0  8136  cfsuc  8137  cff1  8138  cflim2  8143  cfss  8145  cfslb2n  8148  cofsmo  8149  cfsmolem  8150  fin23lem34  8226  fin1a2lem13  8292  axdc3lem2  8331  axdclem  8399  pwcfsdom  8458  wunfi  8596  tskxpss  8647  tskcard  8656  suprzcl  10349  uzwo  10539  uzwoOLD  10540  uzwo2  10541  infmssuzle  10558  infmssuzcl  10559  supxrbnd  10907  supxrgtmnf  10908  supxrre1  10909  supxrre2  10910  supxrss  10911  iccsupr  10997  hashf1lem2  11705  fsum2d  12555  fsumabs  12580  fsumrlim  12590  fsumo1  12591  rpnnen2lem4  12817  rpnnen2lem7  12820  ramub2  13382  ressinbas  13525  ressress  13526  submre  13830  mrcss  13841  mreacs  13883  drsdirfi  14395  clatglbss  14554  ipopos  14586  cntz2ss  15131  ablfac1eulem  15630  subrgint  15890  tgval  17020  unitg  17032  mretopd  17156  ssnei  17174  opnneiss  17182  restdis  17242  restcls  17245  restntr  17246  tgcnp  17317  fbssfi  17869  fgss2  17906  fgcl  17910  supfil  17927  alexsubALTlem3  18080  alexsubALTlem4  18081  cnextcn  18098  ustex3sym  18247  trust  18259  restutop  18267  utop2nei  18280  cfiluweak  18325  blssexps  18456  blssex  18457  mopni3  18524  metss  18538  metcnp3  18570  metustOLD  18597  metust  18598  cfilucfilOLD  18599  cfilucfil  18600  metutopOLD  18612  psmetutop  18613  tgioo  18827  xrsmopn  18843  fsumcn  18900  cncfmptid  18942  iscmet3lem2  19245  caussi  19250  ovolsslem  19380  ovolsscl  19382  ovolssnul  19383  opnmblALT  19495  itgfsum  19718  limcresi  19772  dvmptfsum  19859  plyss  20118  chsupunss  22846  shsupunss  22848  spanss  22850  shslubi  22887  shlub  22916  mdsl1i  23824  mdsl2i  23825  cvmdi  23827  mdslmd1lem1  23828  mdslmd1lem2  23829  mdslmd2i  23833  mdslmd4i  23836  atomli  23885  atcvatlem  23888  chirredlem2  23894  chirredi  23897  mdsymlem5  23910  tpr2rico  24310  sigainb  24519  dya2icoseg2  24628  ballotlem2  24746  cvmlift2lem12  25001  fprod2d  25305  mblfinlem4  26246  ismblfin  26247  opnbnd  26328  fneint  26357  filbcmb  26442  heiborlem10  26529  igenmin  26674  isnacs3  26764  itgoss  27345  sspwimp  29030  sspwimpVD  29031  lssatle  29813  paddss1  30614  paddss2  30615  paddss12  30616  paddssw2  30641  pclssN  30691  pclfinN  30697  polsubN  30704  2polvalN  30711  2polssN  30712  3polN  30713  2pmaplubN  30723  pnonsingN  30730  polsubclN  30749  dihord6apre  32054  dochsscl  32166  mapdordlem2  32435
This theorem was proved from axioms:  ax-1 5  ax-2 6  ax-3 7  ax-mp 8  ax-gen 1555  ax-5 1566  ax-17 1626  ax-9 1666  ax-8 1687  ax-6 1744  ax-7 1749  ax-11 1761  ax-12 1950  ax-ext 2417
This theorem depends on definitions:  df-bi 178  df-an 361  df-tru 1328  df-ex 1551  df-nf 1554  df-sb 1659  df-clab 2423  df-cleq 2429  df-clel 2432  df-in 3327  df-ss 3334
  Copyright terms: Public domain W3C validator