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

Theorem sstr 3348
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 3347 . 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 3312
This theorem is referenced by:  sstrd  3350  sylan9ss  3353  ssdifss  3470  uneqin  3584  ssrnres  5301  relrelss  5385  fco  5592  fssres  5602  ssimaex  5780  dff3  5874  tpostpos2  6492  smores  6606  om00  6810  omeulem2  6818  pmss12g  7032  unblem1  7351  unblem2  7352  unblem3  7353  unblem4  7354  isfinite2  7357  cantnfval2  7614  cantnfle  7616  rankxplim3  7795  alephinit  7966  dfac12lem2  8014  ackbij1lem11  8100  cfeq0  8126  cfsuc  8127  cff1  8128  cflim2  8133  cfss  8135  cfslb2n  8138  cofsmo  8139  cfsmolem  8140  fin23lem34  8216  fin1a2lem13  8282  axdc3lem2  8321  axdclem  8389  pwcfsdom  8448  wunfi  8586  tskxpss  8637  tskcard  8646  suprzcl  10339  uzwo  10529  uzwoOLD  10530  uzwo2  10531  infmssuzle  10548  infmssuzcl  10549  supxrbnd  10897  supxrgtmnf  10898  supxrre1  10899  supxrre2  10900  supxrss  10901  iccsupr  10987  hashf1lem2  11695  fsum2d  12545  fsumabs  12570  fsumrlim  12580  fsumo1  12581  rpnnen2lem4  12807  rpnnen2lem7  12810  ramub2  13372  ressinbas  13515  ressress  13516  submre  13820  mrcss  13831  mreacs  13873  drsdirfi  14385  clatglbss  14544  ipopos  14576  cntz2ss  15121  ablfac1eulem  15620  subrgint  15880  tgval  17010  unitg  17022  mretopd  17146  ssnei  17164  opnneiss  17172  restdis  17232  restcls  17235  restntr  17236  tgcnp  17307  fbssfi  17859  fgss2  17896  fgcl  17900  supfil  17917  alexsubALTlem3  18070  alexsubALTlem4  18071  cnextcn  18088  ustex3sym  18237  trust  18249  restutop  18257  utop2nei  18270  cfiluweak  18315  blssexps  18446  blssex  18447  mopni3  18514  metss  18528  metcnp3  18560  metustOLD  18587  metust  18588  cfilucfilOLD  18589  cfilucfil  18590  metutopOLD  18602  psmetutop  18603  tgioo  18817  xrsmopn  18833  fsumcn  18890  cncfmptid  18932  iscmet3lem2  19235  caussi  19240  ovolsslem  19370  ovolsscl  19372  ovolssnul  19373  opnmblALT  19485  itgfsum  19708  limcresi  19762  dvmptfsum  19849  plyss  20108  chsupunss  22836  shsupunss  22838  spanss  22840  shslubi  22877  shlub  22906  mdsl1i  23814  mdsl2i  23815  cvmdi  23817  mdslmd1lem1  23818  mdslmd1lem2  23819  mdslmd2i  23823  mdslmd4i  23826  atomli  23875  atcvatlem  23878  chirredlem2  23884  chirredi  23887  mdsymlem5  23900  tpr2rico  24300  sigainb  24509  dya2icoseg2  24618  ballotlem2  24736  cvmlift2lem12  24991  fprod2d  25295  mblfinlem3  26209  ismblfin  26210  opnbnd  26282  fneint  26311  filbcmb  26396  heiborlem10  26483  igenmin  26628  isnacs3  26718  itgoss  27300  sspwimp  28931  sspwimpVD  28932  lssatle  29714  paddss1  30515  paddss2  30516  paddss12  30517  paddssw2  30542  pclssN  30592  pclfinN  30598  polsubN  30605  2polvalN  30612  2polssN  30613  3polN  30614  2pmaplubN  30624  pnonsingN  30631  polsubclN  30650  dihord6apre  31955  dochsscl  32067  mapdordlem2  32336
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 2416
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 2422  df-cleq 2428  df-clel 2431  df-in 3319  df-ss 3326
  Copyright terms: Public domain W3C validator