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

Theorem sstr 3497
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 3496 . 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 3461
This theorem was proved from axioms:  ax-mp 5  ax-1 6  ax-2 7  ax-3 8  ax-gen 1605  ax-4 1618  ax-5 1691  ax-6 1734  ax-7 1776  ax-10 1823  ax-11 1828  ax-12 1840  ax-13 1985  ax-ext 2421
This theorem depends on definitions:  df-bi 185  df-an 371  df-tru 1386  df-ex 1600  df-nf 1604  df-sb 1727  df-clab 2429  df-cleq 2435  df-clel 2438  df-in 3468  df-ss 3475
This theorem is referenced by:  sstrd  3499  sylan9ss  3502  ssdifss  3620  uneqin  3734  ssrnres  5435  relrelss  5521  fco  5731  fssres  5741  ssimaex  5923  dff3  6029  tpostpos2  6978  smores  7025  om00  7226  omeulem2  7234  pmss12g  7447  unblem1  7774  unblem2  7775  unblem3  7776  unblem4  7777  isfinite2  7780  cantnfval2  8091  cantnfle  8093  cantnfval2OLD  8121  cantnfleOLD  8123  rankxplim3  8302  alephinit  8479  dfac12lem2  8527  ackbij1lem11  8613  cfeq0  8639  cfsuc  8640  cff1  8641  cflim2  8646  cfss  8648  cfslb2n  8651  cofsmo  8652  cfsmolem  8653  fin23lem34  8729  fin1a2lem13  8795  axdc3lem2  8834  axdclem  8902  pwcfsdom  8961  wunfi  9102  tskxpss  9153  tskcard  9162  suprzcl  10949  uzwo  11155  uzwoOLD  11156  uzwo2  11157  infmssuzle  11175  infmssuzcl  11176  supxrbnd  11531  supxrgtmnf  11532  supxrre1  11533  supxrre2  11534  supxrss  11535  iccsupr  11628  hashf1lem2  12487  fsum2d  13568  fsumabs  13597  fsumrlim  13607  fsumo1  13608  fprod2d  13767  rpnnen2lem4  13933  rpnnen2lem7  13936  ramub2  14514  ressinbas  14675  ressress  14676  submre  14984  mrcss  14995  mreacs  15037  drsdirfi  15546  clatglbss  15736  ipopos  15769  cntz2ss  16349  ablfac1eulem  17102  subrgint  17430  tgval  19434  unitgOLD  19447  mretopd  19571  ssnei  19589  opnneiss  19597  restdis  19657  restcls  19660  restntr  19661  tgcnp  19732  fbssfi  20316  fgss2  20353  fgcl  20357  supfil  20374  alexsubALTlem3  20527  alexsubALTlem4  20528  cnextcn  20545  ustex3sym  20698  trust  20710  restutop  20718  utop2nei  20731  cfiluweak  20776  blssexps  20907  blssex  20908  mopni3  20975  metss  20989  metcnp3  21021  metustOLD  21048  metust  21049  cfilucfilOLD  21050  cfilucfil  21051  metutopOLD  21063  psmetutop  21064  tgioo  21279  xrsmopn  21295  fsumcn  21352  cncfmptid  21394  iscmet3lem2  21709  caussi  21714  ovolsslem  21873  ovolsscl  21875  ovolssnul  21876  opnmblALT  21990  itgfsum  22211  limcresi  22267  dvmptfsum  22354  plyss  22574  chsupunss  26240  shsupunss  26242  spanss  26244  shslubi  26281  shlub  26310  mdsl1i  27218  mdsl2i  27219  cvmdi  27221  mdslmd1lem1  27222  mdslmd1lem2  27223  mdslmd2i  27227  mdslmd4i  27230  atomli  27279  atcvatlem  27282  chirredlem2  27288  chirredi  27291  mdsymlem5  27304  xrge0infss  27558  tpr2rico  27872  sigainb  28114  dya2icoseg2  28227  eulerpartlemn  28298  ballotlem2  28405  cvmlift2lem12  28737  fin2so  30016  mblfinlem4  30030  ismblfin  30031  opnbnd  30119  fneint  30142  filbcmb  30207  heiborlem10  30292  igenmin  30437  isnacs3  30618  itgoss  31088  infmxrss  31446  islptre  31579  gsumlsscl  32846  lincellss  32897  ellcoellss  32906  sspwimp  33586  sspwimpVD  33587  lssatle  34615  paddss1  35416  paddss2  35417  paddss12  35418  paddssw2  35443  pclssN  35493  pclfinN  35499  polsubN  35506  2polvalN  35513  2polssN  35514  3polN  35515  2pmaplubN  35525  pnonsingN  35532  polsubclN  35551  dihord6apre  36858  dochsscl  36970  mapdordlem2  37239
  Copyright terms: Public domain W3C validator