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

Theorem sstr 3472
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 3471 . 2  |-  ( A 
C_  B  ->  ( B  C_  C  ->  A  C_  C ) )
21imp 430 1  |-  ( ( A  C_  B  /\  B  C_  C )  ->  A  C_  C )
Colors of variables: wff setvar class
Syntax hints:    -> wi 4    /\ wa 370    C_ wss 3436
This theorem was proved from axioms:  ax-mp 5  ax-1 6  ax-2 7  ax-3 8  ax-gen 1663  ax-4 1676  ax-5 1752  ax-6 1798  ax-7 1843  ax-10 1891  ax-11 1896  ax-12 1909  ax-13 2057  ax-ext 2401
This theorem depends on definitions:  df-bi 188  df-an 372  df-tru 1440  df-ex 1658  df-nf 1662  df-sb 1791  df-clab 2408  df-cleq 2414  df-clel 2417  df-in 3443  df-ss 3450
This theorem is referenced by:  sstrd  3474  sylan9ss  3477  ssdifss  3596  uneqin  3724  ssrnres  5294  relrelss  5378  fco  5756  fssres  5766  ssimaex  5946  dff3  6050  tpostpos2  7005  smores  7082  om00  7287  omeulem2  7295  pmss12g  7509  unblem1  7832  unblem2  7833  unblem3  7834  unblem4  7835  isfinite2  7838  cantnfval2  8182  cantnfle  8184  rankxplim3  8360  alephinit  8533  dfac12lem2  8581  ackbij1lem11  8667  cfeq0  8693  cfsuc  8694  cff1  8695  cflim2  8700  cfss  8702  cfslb2n  8705  cofsmo  8706  cfsmolem  8707  fin23lem34  8783  fin1a2lem13  8849  axdc3lem2  8888  axdclem  8956  pwcfsdom  9015  wunfi  9153  tskxpss  9204  tskcard  9213  suprzcl  11022  uzwo  11229  uzwo2  11230  infssuzle  11251  infssuzcl  11252  infmssuzleOLD  11253  infmssuzclOLD  11254  supxrbnd  11621  supxrgtmnf  11622  supxrre1  11623  supxrre2  11624  supxrss  11625  infxrss  11635  infmxrssOLD  11636  iccsupr  11734  hashf1lem2  12623  trclun  13078  fsum2d  13831  fsumabs  13860  fsumrlim  13870  fsumo1  13871  fprod2d  14034  rpnnen2lem4  14269  rpnnen2lem7  14272  ramub2  14970  ressinbas  15184  ressress  15186  submre  15510  mrcss  15521  mreacs  15563  drsdirfi  16182  clatglbss  16372  ipopos  16405  cntz2ss  16985  ablfac1eulem  17704  subrgint  18029  tgval  19968  unitgOLD  19981  mretopd  20106  ssnei  20124  opnneiss  20132  restdis  20192  restcls  20195  restntr  20196  tgcnp  20267  fbssfi  20850  fgss2  20887  fgcl  20891  supfil  20908  alexsubALTlem3  21062  alexsubALTlem4  21063  cnextcn  21080  ustex3sym  21230  trust  21242  restutop  21250  utop2nei  21263  cfiluweak  21308  blssexps  21439  blssex  21440  mopni3  21507  metss  21521  metcnp3  21553  metust  21571  cfilucfil  21572  psmetutop  21580  tgioo  21812  xrsmopn  21828  fsumcn  21900  cncfmptid  21942  iscmet3lem2  22260  caussi  22265  ovolsslem  22435  ovolsscl  22437  ovolssnul  22438  opnmblALT  22559  itgfsum  22782  limcresi  22838  dvmptfsum  22925  plyss  23151  chsupunss  26995  shsupunss  26997  spanss  26999  shslubi  27036  shlub  27065  mdsl1i  27972  mdsl2i  27973  cvmdi  27975  mdslmd1lem1  27976  mdslmd1lem2  27977  mdslmd2i  27981  mdslmd4i  27984  atomli  28033  atcvatlem  28036  chirredlem2  28042  chirredi  28045  mdsymlem5  28058  xrge0infss  28346  xrge0infssOLD  28347  tpr2rico  28726  sigainb  28966  dya2icoseg2  29108  omssubadd  29136  omssubaddOLD  29140  eulerpartlemn  29222  ballotlem2  29329  cvmlift2lem12  30045  opnbnd  30986  fneint  31009  dissneqlem  31706  fin2so  31896  mblfinlem4  31944  ismblfin  31945  filbcmb  32031  heiborlem10  32116  igenmin  32261  lssatle  32550  paddss1  33351  paddss2  33352  paddss12  33353  paddssw2  33378  pclssN  33428  pclfinN  33434  polsubN  33441  2polvalN  33448  2polssN  33449  3polN  33450  2pmaplubN  33460  pnonsingN  33467  polsubclN  33486  dihord6apre  34793  dochsscl  34905  mapdordlem2  35174  isnacs3  35521  itgoss  35999  sspwimp  37288  sspwimpVD  37289  islptre  37639  ausgrumgri  39049  nbuhgr  39178  gsumlsscl  39790  lincellss  39841  ellcoellss  39850
  Copyright terms: Public domain W3C validator