Theorem sstr 4017

Description: Transitivity of subclass relationship. Theorem 6 of [Suppes] p. 23. (Contributed by NM, 5-Sep-2003.)

Assertion

Ref	Expression
sstr	⊢ ((𝐴 ⊆ 𝐵 ∧ 𝐵 ⊆ 𝐶) → 𝐴 ⊆ 𝐶)

Proof of Theorem sstr

Step	Hyp	Ref	Expression
1		sstr2 4015	. 2 ⊢ (𝐴 ⊆ 𝐵 → (𝐵 ⊆ 𝐶 → 𝐴 ⊆ 𝐶))
2	1	imp 406	1 ⊢ ((𝐴 ⊆ 𝐵 ∧ 𝐵 ⊆ 𝐶) → 𝐴 ⊆ 𝐶)

Syntax hints:   → wi 4   ∧ wa 395   ⊆ wss 3976

This theorem was proved from axioms:  ax-mp 5  ax-1 6  ax-2 7  ax-3 8  ax-gen 1793  ax-4 1807

This theorem depends on definitions:  df-bi 207  df-an 396  df-ss 3993

This theorem is referenced by:  sstrd  4019  sylan9ss  4022  ssdifss  4163  uneqin  4308  intss2  5131  ssrnres  6209  relrelss  6304  fcof  6770  fcoOLD  6772  fssres  6787  ssimaex  7007  dff3  7134  tpostpos2  8288  smores  8408  om00  8631  omeulem2  8639  cofonr  8730  naddunif  8749  pmss12g  8927  unblem1  9356  unblem2  9357  unblem3  9358  unblem4  9359  isfinite2  9362  cantnfval2  9738  cantnfle  9740  rankxplim3  9950  alephinit  10164  dfac12lem2  10214  ackbij1lem11  10298  cfeq0  10325  cfsuc  10326  cff1  10327  cflim2  10332  cfss  10334  cfslb2n  10337  cofsmo  10338  cfsmolem  10339  fin23lem34  10415  fin1a2lem13  10481  axdc3lem2  10520  axdclem  10588  pwcfsdom  10652  wunfi  10790  tskxpss  10841  tskcard  10850  suprzcl  12723  uzwo  12976  uzwo2  12977  infssuzle  12996  infssuzcl  12997  supxrbnd  13390  supxrgtmnf  13391  supxrre1  13392  supxrre2  13393  supxrss  13394  infxrss  13401  iccsupr  13502  hashf1lem2  14505  trclun  15063  fsum2d  15819  fsumabs  15849  fsumrlim  15859  fsumo1  15860  fprod2d  16029  rpnnen2lem4  16265  rpnnen2lem7  16268  ramub2  17061  ressinbas  17304  ressress  17307  submre  17663  mrcss  17674  mreacs  17716  drsdirfi  18375  clatglbss  18589  ipopos  18606  cntz2ss  19375  pgrpsubgsymg  19451  ablfac1eulem  20116  subrngint  20586  subrgint  20623  tgval  22983  mretopd  23121  ssnei  23139  opnneiss  23147  restdis  23207  restcls  23210  restntr  23211  tgcnp  23282  fbssfi  23866  fgss2  23903  fgcl  23907  supfil  23924  alexsubALTlem3  24078  alexsubALTlem4  24079  cnextcn  24096  ustex3sym  24247  trust  24259  restutop  24267  utop2nei  24280  cfiluweak  24325  blssexps  24457  blssex  24458  mopni3  24528  metss  24542  metcnp3  24574  metust  24592  cfilucfil  24593  psmetutop  24601  tgioo  24837  xrsmopn  24853  fsumcn  24913  cncfmptid  24958  iscmet3lem2  25345  caussi  25350  ovolsslem  25538  ovolsscl  25540  ovolssnul  25541  opnmblALT  25657  itgfsum  25882  limcresi  25940  dvmptfsum  26033  plyss  26258  madebdayim  27944  cofcutrtime  27979  nbuhgr  29378  chsupunss  31376  shsupunss  31378  spanss  31380  shslubi  31417  shlub  31446  mdsl1i  32353  mdsl2i  32354  cvmdi  32356  mdslmd1lem1  32357  mdslmd1lem2  32358  mdslmd2i  32362  mdslmd4i  32365  atomli  32414  atcvatlem  32417  chirredlem2  32423  chirredi  32426  mdsymlem5  32439  xrge0infss  32767  tpr2rico  33858  sigainb  34100  dya2icoseg2  34243  omssubadd  34265  eulerpartlemn  34346  ballotlem2  34453  nummin  35067  cvmlift2lem12  35282  opnbnd  36291  fneint  36314  dissneqlem  37306  inunissunidif  37341  pibt2  37383  fin2so  37567  matunitlindflem1  37576  mblfinlem4  37620  ismblfin  37621  filbcmb  37700  heiborlem10  37780  igenmin  38024  lssatle  38971  paddss1  39774  paddss2  39775  paddss12  39776  paddssw2  39801  pclssN  39851  pclfinN  39857  polsubN  39864  2polvalN  39871  2polssN  39872  3polN  39873  2pmaplubN  39883  pnonsingN  39890  polsubclN  39909  dihord6apre  41213  dochsscl  41325  mapdordlem2  41594  isnacs3  42666  itgoss  43120  ofoaid1  43320  ofoaid2  43321  sspwimp  44889  sspwimpVD  44890  nsstr  44997  islptre  45540  gsumlsscl  48108  lincellss  48155  ellcoellss  48164