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

Theorem sstr 3316
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 3315 . 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 3280
This theorem is referenced by:  sstrd  3318  sylan9ss  3321  ssdifss  3438  uneqin  3552  ssrnres  5268  relrelss  5352  fco  5559  fssres  5569  ssimaex  5747  dff3  5841  tpostpos2  6459  smores  6573  om00  6777  omeulem2  6785  pmss12g  6999  unblem1  7318  unblem2  7319  unblem3  7320  unblem4  7321  isfinite2  7324  cantnfval2  7580  cantnfle  7582  rankxplim3  7761  alephinit  7932  dfac12lem2  7980  ackbij1lem11  8066  cfeq0  8092  cfsuc  8093  cff1  8094  cflim2  8099  cfss  8101  cfslb2n  8104  cofsmo  8105  cfsmolem  8106  fin23lem34  8182  fin1a2lem13  8248  axdc3lem2  8287  axdclem  8355  pwcfsdom  8414  wunfi  8552  tskxpss  8603  tskcard  8612  suprzcl  10305  uzwo  10495  uzwoOLD  10496  uzwo2  10497  infmssuzle  10514  infmssuzcl  10515  supxrbnd  10863  supxrgtmnf  10864  supxrre1  10865  supxrre2  10866  supxrss  10867  iccsupr  10953  hashf1lem2  11660  fsum2d  12510  fsumabs  12535  fsumrlim  12545  fsumo1  12546  rpnnen2lem4  12772  rpnnen2lem7  12775  ramub2  13337  ressinbas  13480  ressress  13481  submre  13785  mrcss  13796  mreacs  13838  drsdirfi  14350  clatglbss  14509  ipopos  14541  cntz2ss  15086  ablfac1eulem  15585  subrgint  15845  tgval  16975  unitg  16987  mretopd  17111  ssnei  17129  opnneiss  17137  restdis  17196  restcls  17199  restntr  17200  tgcnp  17271  fbssfi  17822  fgss2  17859  fgcl  17863  supfil  17880  alexsubALTlem3  18033  alexsubALTlem4  18034  cnextcn  18051  ustex3sym  18200  trust  18212  restutop  18220  utop2nei  18233  cfiluweak  18278  blssexps  18409  blssex  18410  mopni3  18477  metss  18491  metcnp3  18523  metustOLD  18550  metust  18551  cfilucfilOLD  18552  cfilucfil  18553  metutopOLD  18565  psmetutop  18566  tgioo  18780  xrsmopn  18796  fsumcn  18853  cncfmptid  18895  iscmet3lem2  19198  caussi  19203  ovolsslem  19333  ovolsscl  19335  ovolssnul  19336  opnmblALT  19448  itgfsum  19671  limcresi  19725  dvmptfsum  19812  plyss  20071  chsupunss  22799  shsupunss  22801  spanss  22803  shslubi  22840  shlub  22869  mdsl1i  23777  mdsl2i  23778  cvmdi  23780  mdslmd1lem1  23781  mdslmd1lem2  23782  mdslmd2i  23786  mdslmd4i  23789  atomli  23838  atcvatlem  23841  chirredlem2  23847  chirredi  23850  mdsymlem5  23863  tpr2rico  24263  sigainb  24472  dya2icoseg2  24581  ballotlem2  24699  cvmlift2lem12  24954  fprod2d  25258  mblfinlem3  26145  ismblfin  26146  opnbnd  26218  fneint  26247  filbcmb  26332  heiborlem10  26419  igenmin  26564  isnacs3  26654  itgoss  27236  sspwimp  28739  sspwimpVD  28740  lssatle  29498  paddss1  30299  paddss2  30300  paddss12  30301  paddssw2  30326  pclssN  30376  pclfinN  30382  polsubN  30389  2polvalN  30396  2polssN  30397  3polN  30398  2pmaplubN  30408  pnonsingN  30415  polsubclN  30434  dihord6apre  31739  dochsscl  31851  mapdordlem2  32120
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 2385
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 2391  df-cleq 2397  df-clel 2400  df-in 3287  df-ss 3294
  Copyright terms: Public domain W3C validator