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

Theorem sstr 3352
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 3351 . 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 3316
This theorem was proved from axioms:  ax-mp 5  ax-1 6  ax-2 7  ax-3 8  ax-gen 1594  ax-4 1605  ax-5 1669  ax-6 1707  ax-7 1727  ax-10 1774  ax-11 1779  ax-12 1791  ax-13 1942  ax-ext 2414
This theorem depends on definitions:  df-bi 185  df-an 371  df-ex 1590  df-nf 1593  df-sb 1700  df-clab 2420  df-cleq 2426  df-clel 2429  df-in 3323  df-ss 3330
This theorem is referenced by:  sstrd  3354  sylan9ss  3357  ssdifss  3475  uneqin  3589  ssrnres  5264  relrelss  5349  fco  5556  fssres  5566  ssimaex  5744  dff3  5844  tpostpos2  6755  smores  6799  om00  7002  omeulem2  7010  pmss12g  7227  unblem1  7552  unblem2  7553  unblem3  7554  unblem4  7555  isfinite2  7558  cantnfval2  7865  cantnfle  7867  cantnfval2OLD  7895  cantnfleOLD  7897  rankxplim3  8076  alephinit  8253  dfac12lem2  8301  ackbij1lem11  8387  cfeq0  8413  cfsuc  8414  cff1  8415  cflim2  8420  cfss  8422  cfslb2n  8425  cofsmo  8426  cfsmolem  8427  fin23lem34  8503  fin1a2lem13  8569  axdc3lem2  8608  axdclem  8676  pwcfsdom  8735  wunfi  8876  tskxpss  8927  tskcard  8936  suprzcl  10709  uzwo  10905  uzwoOLD  10906  uzwo2  10907  infmssuzle  10925  infmssuzcl  10926  supxrbnd  11279  supxrgtmnf  11280  supxrre1  11281  supxrre2  11282  supxrss  11283  iccsupr  11370  hashf1lem2  12193  fsum2d  13222  fsumabs  13247  fsumrlim  13257  fsumo1  13258  rpnnen2lem4  13483  rpnnen2lem7  13486  ramub2  14058  ressinbas  14217  ressress  14218  submre  14526  mrcss  14537  mreacs  14579  drsdirfi  15091  clatglbss  15280  ipopos  15313  cntz2ss  15830  ablfac1eulem  16547  subrgint  16811  tgval  18402  unitg  18414  mretopd  18538  ssnei  18556  opnneiss  18564  restdis  18624  restcls  18627  restntr  18628  tgcnp  18699  fbssfi  19252  fgss2  19289  fgcl  19293  supfil  19310  alexsubALTlem3  19463  alexsubALTlem4  19464  cnextcn  19481  ustex3sym  19634  trust  19646  restutop  19654  utop2nei  19667  cfiluweak  19712  blssexps  19843  blssex  19844  mopni3  19911  metss  19925  metcnp3  19957  metustOLD  19984  metust  19985  cfilucfilOLD  19986  cfilucfil  19987  metutopOLD  19999  psmetutop  20000  tgioo  20215  xrsmopn  20231  fsumcn  20288  cncfmptid  20330  iscmet3lem2  20645  caussi  20650  ovolsslem  20809  ovolsscl  20811  ovolssnul  20812  opnmblALT  20925  itgfsum  21146  limcresi  21202  dvmptfsum  21289  plyss  21552  chsupunss  24570  shsupunss  24572  spanss  24574  shslubi  24611  shlub  24640  mdsl1i  25548  mdsl2i  25549  cvmdi  25551  mdslmd1lem1  25552  mdslmd1lem2  25553  mdslmd2i  25557  mdslmd4i  25560  atomli  25609  atcvatlem  25612  chirredlem2  25618  chirredi  25621  mdsymlem5  25634  tpr2rico  26196  sigainb  26433  dya2icoseg2  26547  eulerpartlemn  26612  ballotlem2  26719  cvmlift2lem12  27051  fprod2d  27339  fin2so  28260  mblfinlem4  28275  ismblfin  28276  opnbnd  28364  fneint  28393  filbcmb  28478  heiborlem10  28563  igenmin  28708  isnacs3  28891  itgoss  29365  gsumlsscl  30625  lincellss  30669  ellcoellss  30678  sspwimp  31356  sspwimpVD  31357  lssatle  32233  paddss1  33034  paddss2  33035  paddss12  33036  paddssw2  33061  pclssN  33111  pclfinN  33117  polsubN  33124  2polvalN  33131  2polssN  33132  3polN  33133  2pmaplubN  33143  pnonsingN  33150  polsubclN  33169  dihord6apre  34474  dochsscl  34586  mapdordlem2  34855
  Copyright terms: Public domain W3C validator