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

Theorem sstr 3512
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 3511 . 2  |-  ( A 
C_  B  ->  ( B  C_  C  ->  A  C_  C ) )
21imp 429 1  |-  ( ( A  C_  B  /\  B  C_  C )  ->  A  C_  C )
Colors of variables: wff setvar class
Syntax hints:    -> wi 4    /\ wa 369    C_ wss 3476
This theorem was proved from axioms:  ax-mp 5  ax-1 6  ax-2 7  ax-3 8  ax-gen 1601  ax-4 1612  ax-5 1680  ax-6 1719  ax-7 1739  ax-10 1786  ax-11 1791  ax-12 1803  ax-13 1968  ax-ext 2445
This theorem depends on definitions:  df-bi 185  df-an 371  df-tru 1382  df-ex 1597  df-nf 1600  df-sb 1712  df-clab 2453  df-cleq 2459  df-clel 2462  df-in 3483  df-ss 3490
This theorem is referenced by:  sstrd  3514  sylan9ss  3517  ssdifss  3635  uneqin  3749  ssrnres  5445  relrelss  5531  fco  5741  fssres  5751  ssimaex  5932  dff3  6034  tpostpos2  6976  smores  7023  om00  7224  omeulem2  7232  pmss12g  7445  unblem1  7772  unblem2  7773  unblem3  7774  unblem4  7775  isfinite2  7778  cantnfval2  8088  cantnfle  8090  cantnfval2OLD  8118  cantnfleOLD  8120  rankxplim3  8299  alephinit  8476  dfac12lem2  8524  ackbij1lem11  8610  cfeq0  8636  cfsuc  8637  cff1  8638  cflim2  8643  cfss  8645  cfslb2n  8648  cofsmo  8649  cfsmolem  8650  fin23lem34  8726  fin1a2lem13  8792  axdc3lem2  8831  axdclem  8899  pwcfsdom  8958  wunfi  9099  tskxpss  9150  tskcard  9159  suprzcl  10940  uzwo  11144  uzwoOLD  11145  uzwo2  11146  infmssuzle  11164  infmssuzcl  11165  supxrbnd  11520  supxrgtmnf  11521  supxrre1  11522  supxrre2  11523  supxrss  11524  iccsupr  11617  hashf1lem2  12471  fsum2d  13549  fsumabs  13578  fsumrlim  13588  fsumo1  13589  rpnnen2lem4  13812  rpnnen2lem7  13815  ramub2  14391  ressinbas  14551  ressress  14552  submre  14860  mrcss  14871  mreacs  14913  drsdirfi  15425  clatglbss  15614  ipopos  15647  cntz2ss  16175  ablfac1eulem  16925  subrgint  17251  tgval  19251  unitg  19263  mretopd  19387  ssnei  19405  opnneiss  19413  restdis  19473  restcls  19476  restntr  19477  tgcnp  19548  fbssfi  20101  fgss2  20138  fgcl  20142  supfil  20159  alexsubALTlem3  20312  alexsubALTlem4  20313  cnextcn  20330  ustex3sym  20483  trust  20495  restutop  20503  utop2nei  20516  cfiluweak  20561  blssexps  20692  blssex  20693  mopni3  20760  metss  20774  metcnp3  20806  metustOLD  20833  metust  20834  cfilucfilOLD  20835  cfilucfil  20836  metutopOLD  20848  psmetutop  20849  tgioo  21064  xrsmopn  21080  fsumcn  21137  cncfmptid  21179  iscmet3lem2  21494  caussi  21499  ovolsslem  21658  ovolsscl  21660  ovolssnul  21661  opnmblALT  21775  itgfsum  21996  limcresi  22052  dvmptfsum  22139  plyss  22359  chsupunss  25966  shsupunss  25968  spanss  25970  shslubi  26007  shlub  26036  mdsl1i  26944  mdsl2i  26945  cvmdi  26947  mdslmd1lem1  26948  mdslmd1lem2  26949  mdslmd2i  26953  mdslmd4i  26956  atomli  27005  atcvatlem  27008  chirredlem2  27014  chirredi  27017  mdsymlem5  27030  xrge0infss  27276  tpr2rico  27558  sigainb  27804  dya2icoseg2  27917  eulerpartlemn  27988  ballotlem2  28095  cvmlift2lem12  28427  fprod2d  28716  fin2so  29645  mblfinlem4  29659  ismblfin  29660  opnbnd  29748  fneint  29777  filbcmb  29862  heiborlem10  29947  igenmin  30092  isnacs3  30274  itgoss  30745  infmxrss  31097  islptre  31189  icccncfext  31254  gsumlsscl  32075  lincellss  32126  ellcoellss  32135  sspwimp  32816  sspwimpVD  32817  lssatle  33830  paddss1  34631  paddss2  34632  paddss12  34633  paddssw2  34658  pclssN  34708  pclfinN  34714  polsubN  34721  2polvalN  34728  2polssN  34729  3polN  34730  2pmaplubN  34740  pnonsingN  34747  polsubclN  34766  dihord6apre  36071  dochsscl  36183  mapdordlem2  36452
  Copyright terms: Public domain W3C validator