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

Theorem sstr 3324
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 3323 . 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 3288
This theorem is referenced by:  sstrd  3326  sylan9ss  3329  ssdifss  3446  uneqin  3560  ssrnres  5276  relrelss  5360  fco  5567  fssres  5577  ssimaex  5755  dff3  5849  tpostpos2  6467  smores  6581  om00  6785  omeulem2  6793  pmss12g  7007  unblem1  7326  unblem2  7327  unblem3  7328  unblem4  7329  isfinite2  7332  cantnfval2  7588  cantnfle  7590  rankxplim3  7769  alephinit  7940  dfac12lem2  7988  ackbij1lem11  8074  cfeq0  8100  cfsuc  8101  cff1  8102  cflim2  8107  cfss  8109  cfslb2n  8112  cofsmo  8113  cfsmolem  8114  fin23lem34  8190  fin1a2lem13  8256  axdc3lem2  8295  axdclem  8363  pwcfsdom  8422  wunfi  8560  tskxpss  8611  tskcard  8620  suprzcl  10313  uzwo  10503  uzwoOLD  10504  uzwo2  10505  infmssuzle  10522  infmssuzcl  10523  supxrbnd  10871  supxrgtmnf  10872  supxrre1  10873  supxrre2  10874  supxrss  10875  iccsupr  10961  hashf1lem2  11668  fsum2d  12518  fsumabs  12543  fsumrlim  12553  fsumo1  12554  rpnnen2lem4  12780  rpnnen2lem7  12783  ramub2  13345  ressinbas  13488  ressress  13489  submre  13793  mrcss  13804  mreacs  13846  drsdirfi  14358  clatglbss  14517  ipopos  14549  cntz2ss  15094  ablfac1eulem  15593  subrgint  15853  tgval  16983  unitg  16995  mretopd  17119  ssnei  17137  opnneiss  17145  restdis  17204  restcls  17207  restntr  17208  tgcnp  17279  fbssfi  17830  fgss2  17867  fgcl  17871  supfil  17888  alexsubALTlem3  18041  alexsubALTlem4  18042  cnextcn  18059  ustex3sym  18208  trust  18220  restutop  18228  utop2nei  18241  cfiluweak  18286  blssexps  18417  blssex  18418  mopni3  18485  metss  18499  metcnp3  18531  metustOLD  18558  metust  18559  cfilucfilOLD  18560  cfilucfil  18561  metutopOLD  18573  psmetutop  18574  tgioo  18788  xrsmopn  18804  fsumcn  18861  cncfmptid  18903  iscmet3lem2  19206  caussi  19211  ovolsslem  19341  ovolsscl  19343  ovolssnul  19344  opnmblALT  19456  itgfsum  19679  limcresi  19733  dvmptfsum  19820  plyss  20079  chsupunss  22807  shsupunss  22809  spanss  22811  shslubi  22848  shlub  22877  mdsl1i  23785  mdsl2i  23786  cvmdi  23788  mdslmd1lem1  23789  mdslmd1lem2  23790  mdslmd2i  23794  mdslmd4i  23797  atomli  23846  atcvatlem  23849  chirredlem2  23855  chirredi  23858  mdsymlem5  23871  tpr2rico  24271  sigainb  24480  dya2icoseg2  24589  ballotlem2  24707  cvmlift2lem12  24962  fprod2d  25266  mblfinlem3  26153  ismblfin  26154  opnbnd  26226  fneint  26255  filbcmb  26340  heiborlem10  26427  igenmin  26572  isnacs3  26662  itgoss  27244  sspwimp  28748  sspwimpVD  28749  lssatle  29510  paddss1  30311  paddss2  30312  paddss12  30313  paddssw2  30338  pclssN  30388  pclfinN  30394  polsubN  30401  2polvalN  30408  2polssN  30409  3polN  30410  2pmaplubN  30420  pnonsingN  30427  polsubclN  30446  dihord6apre  31751  dochsscl  31863  mapdordlem2  32132
This theorem was proved from axioms:  ax-1 5  ax-2 6  ax-3 7  ax-mp 8  ax-gen 1552  ax-5 1563  ax-17 1623  ax-9 1662  ax-8 1683  ax-6 1740  ax-7 1745  ax-11 1757  ax-12 1946  ax-ext 2393
This theorem depends on definitions:  df-bi 178  df-an 361  df-tru 1325  df-ex 1548  df-nf 1551  df-sb 1656  df-clab 2399  df-cleq 2405  df-clel 2408  df-in 3295  df-ss 3302
  Copyright terms: Public domain W3C validator