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

Theorem sstr 3263
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 3262 . 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 3228
This theorem is referenced by:  sstrd  3265  sylan9ss  3268  ssdifss  3383  uneqin  3496  ssrnres  5195  relrelss  5275  fco  5478  fssres  5488  ssimaex  5664  dff3  5753  tpostpos2  6339  smores  6453  om00  6657  omeulem2  6665  pmss12g  6879  unblem1  7196  unblem2  7197  unblem3  7198  unblem4  7199  isfinite2  7202  cantnfval2  7457  cantnfle  7459  rankxplim3  7638  alephinit  7809  dfac12lem2  7857  ackbij1lem11  7943  cfeq0  7969  cfsuc  7970  cff1  7971  cflim2  7976  cfss  7978  cfslb2n  7981  cofsmo  7982  cfsmolem  7983  fin23lem34  8059  fin1a2lem13  8125  axdc3lem2  8164  axdclem  8233  pwcfsdom  8292  wunfi  8430  tskxpss  8481  tskcard  8490  suprzcl  10180  uzwo  10370  uzwoOLD  10371  uzwo2  10372  infmssuzle  10389  infmssuzcl  10390  supxrbnd  10736  supxrgtmnf  10737  supxrre1  10738  supxrre2  10739  supxrss  10740  iccsupr  10825  hashf1lem2  11484  fsum2d  12325  fsumabs  12350  fsumrlim  12360  fsumo1  12361  rpnnen2lem4  12587  rpnnen2lem7  12590  ramub2  13152  ressinbas  13295  ressress  13296  submre  13600  mrcss  13611  mreacs  13653  drsdirfi  14165  clatglbss  14324  ipopos  14356  cntz2ss  14901  ablfac1eulem  15400  subrgint  15660  tgval  16793  unitg  16805  mretopd  16929  ssnei  16947  opnneiss  16955  restdis  17009  restcls  17011  restntr  17012  tgcnp  17083  fbssfi  17628  fgss2  17665  fgcl  17669  supfil  17686  alexsubALTlem3  17839  alexsubALTlem4  17840  blssex  18069  mopni3  18136  metss  18150  metcnp3  18182  tgioo  18398  xrsmopn  18414  fsumcn  18471  cncfmptid  18513  iscmet3lem2  18816  caussi  18821  ovolsslem  18941  ovolsscl  18943  ovolssnul  18944  opnmblALT  19056  itgfsum  19279  limcresi  19333  dvmptfsum  19420  plyss  19679  chsupunss  22031  shsupunss  22033  spanss  22035  shslubi  22072  shlub  22101  mdsl1i  23009  mdsl2i  23010  cvmdi  23012  mdslmd1lem1  23013  mdslmd1lem2  23014  mdslmd2i  23018  mdslmd4i  23021  atomli  23070  atcvatlem  23073  chirredlem2  23079  chirredi  23082  mdsymlem5  23095  tpr2rico  23466  cnextcn  23504  trust  23533  restutop  23541  metust  23602  cfilucfil  23603  metutop  23611  sigainb  23785  insiga  23786  dya2icoseg2  23892  ballotlem2  23995  cvmlift2lem12  24249  opnbnd  25567  fneint  25601  filbcmb  25756  lpss2  25792  heiborlem10  25867  igenmin  26012  isnacs3  26108  itgoss  26691  itgsinexplem1  27071  itgsinexp  27072  stoweidlem34  27106  stoweidlem57  27129  stoweidlem59  27131  sspwimp  28439  sspwimpVD  28440  lssatle  29257  paddss1  30058  paddss2  30059  paddss12  30060  paddssw2  30085  pclssN  30135  pclfinN  30141  polsubN  30148  2polvalN  30155  2polssN  30156  3polN  30157  2pmaplubN  30167  pnonsingN  30174  polsubclN  30193  dihord6apre  31498  dochsscl  31610  mapdordlem2  31879
This theorem was proved from axioms:  ax-1 5  ax-2 6  ax-3 7  ax-mp 8  ax-gen 1546  ax-5 1557  ax-17 1616  ax-9 1654  ax-8 1675  ax-6 1729  ax-7 1734  ax-11 1746  ax-12 1930  ax-ext 2339
This theorem depends on definitions:  df-bi 177  df-an 360  df-tru 1319  df-ex 1542  df-nf 1545  df-sb 1649  df-clab 2345  df-cleq 2351  df-clel 2354  df-in 3235  df-ss 3242
  Copyright terms: Public domain W3C validator