Theorem sstr 3992

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 3990	. 2 ⊢ (𝐴 ⊆ 𝐵 → (𝐵 ⊆ 𝐶 → 𝐴 ⊆ 𝐶))
2	1	imp 406	1 ⊢ ((𝐴 ⊆ 𝐵 ∧ 𝐵 ⊆ 𝐶) → 𝐴 ⊆ 𝐶)

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

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

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

This theorem is referenced by:  sstrd  3994  sylan9ss  3997  ssdifss  4140  uneqin  4289  intss2  5108  ssrnres  6198  relrelss  6293  fcof  6759  fssres  6774  ssimaex  6994  dff3  7120  tpostpos2  8272  smores  8392  om00  8613  omeulem2  8621  cofonr  8712  naddunif  8731  pmss12g  8909  unblem1  9328  unblem2  9329  unblem3  9330  unblem4  9331  isfinite2  9334  cantnfval2  9709  cantnfle  9711  rankxplim3  9921  alephinit  10135  dfac12lem2  10185  ackbij1lem11  10269  cfeq0  10296  cfsuc  10297  cff1  10298  cflim2  10303  cfss  10305  cfslb2n  10308  cofsmo  10309  cfsmolem  10310  fin23lem34  10386  fin1a2lem13  10452  axdc3lem2  10491  axdclem  10559  pwcfsdom  10623  wunfi  10761  tskxpss  10812  tskcard  10821  suprzcl  12698  uzwo  12953  uzwo2  12954  infssuzle  12973  infssuzcl  12974  supxrbnd  13370  supxrgtmnf  13371  supxrre1  13372  supxrre2  13373  supxrss  13374  infxrss  13381  iccsupr  13482  hashf1lem2  14495  trclun  15053  fsum2d  15807  fsumabs  15837  fsumrlim  15847  fsumo1  15848  fprod2d  16017  rpnnen2lem4  16253  rpnnen2lem7  16256  ramub2  17052  ressinbas  17291  ressress  17293  submre  17648  mrcss  17659  mreacs  17701  drsdirfi  18351  clatglbss  18564  ipopos  18581  cntz2ss  19353  pgrpsubgsymg  19427  ablfac1eulem  20092  subrngint  20560  subrgint  20595  tgval  22962  mretopd  23100  ssnei  23118  opnneiss  23126  restdis  23186  restcls  23189  restntr  23190  tgcnp  23261  fbssfi  23845  fgss2  23882  fgcl  23886  supfil  23903  alexsubALTlem3  24057  alexsubALTlem4  24058  cnextcn  24075  ustex3sym  24226  trust  24238  restutop  24246  utop2nei  24259  cfiluweak  24304  blssexps  24436  blssex  24437  mopni3  24507  metss  24521  metcnp3  24553  metust  24571  cfilucfil  24572  psmetutop  24580  tgioo  24817  xrsmopn  24834  fsumcn  24894  cncfmptid  24939  iscmet3lem2  25326  caussi  25331  ovolsslem  25519  ovolsscl  25521  ovolssnul  25522  opnmblALT  25638  itgfsum  25862  limcresi  25920  dvmptfsum  26013  plyss  26238  madebdayim  27926  cofcutrtime  27961  nbuhgr  29360  chsupunss  31363  shsupunss  31365  spanss  31367  shslubi  31404  shlub  31433  mdsl1i  32340  mdsl2i  32341  cvmdi  32343  mdslmd1lem1  32344  mdslmd1lem2  32345  mdslmd2i  32349  mdslmd4i  32352  atomli  32401  atcvatlem  32404  chirredlem2  32410  chirredi  32413  mdsymlem5  32426  xrge0infss  32764  tpr2rico  33911  sigainb  34137  dya2icoseg2  34280  omssubadd  34302  eulerpartlemn  34383  ballotlem2  34491  nummin  35105  cvmlift2lem12  35319  opnbnd  36326  fneint  36349  dissneqlem  37341  inunissunidif  37376  pibt2  37418  fin2so  37614  matunitlindflem1  37623  mblfinlem4  37667  ismblfin  37668  filbcmb  37747  heiborlem10  37827  igenmin  38071  lssatle  39016  paddss1  39819  paddss2  39820  paddss12  39821  paddssw2  39846  pclssN  39896  pclfinN  39902  polsubN  39909  2polvalN  39916  2polssN  39917  3polN  39918  2pmaplubN  39928  pnonsingN  39935  polsubclN  39954  dihord6apre  41258  dochsscl  41370  mapdordlem2  41639  isnacs3  42721  itgoss  43175  ofoaid1  43371  ofoaid2  43372  sspwimp  44938  sspwimpVD  44939  nsstr  45100  islptre  45634  gsumlsscl  48296  lincellss  48343  ellcoellss  48352