Theorem sstr 3943

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

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

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

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

This theorem is referenced by:  sstrd  3945  sylan9ss  3948  ssdifss  4093  uneqin  4242  intss2  5064  ssrnres  6137  relrelss  6232  fcof  6686  fssres  6701  ssimaex  6920  dff3  7047  tpostpos2  8192  smores  8287  om00  8505  omeulem2  8513  cofonr  8605  naddunif  8624  pmss12g  8812  unblem1  9197  unblem2  9198  unblem3  9199  unblem4  9200  isfinite2  9203  cantnfval2  9583  cantnfle  9585  rankxplim3  9798  alephinit  10010  dfac12lem2  10060  ackbij1lem11  10144  cfeq0  10171  cfsuc  10172  cff1  10173  cflim2  10178  cfss  10180  cfslb2n  10183  cofsmo  10184  cfsmolem  10185  fin23lem34  10261  fin1a2lem13  10327  axdc3lem2  10366  axdclem  10434  pwcfsdom  10499  wunfi  10637  tskxpss  10688  tskcard  10697  suprzcl  12577  uzwo  12829  uzwo2  12830  infssuzle  12849  infssuzcl  12850  supxrbnd  13248  supxrgtmnf  13249  supxrre1  13250  supxrre2  13251  supxrss  13252  infxrss  13260  iccsupr  13363  hashf1lem2  14384  trclun  14942  fsum2d  15699  fsumabs  15729  fsumrlim  15739  fsumo1  15740  fprod2d  15909  rpnnen2lem4  16147  rpnnen2lem7  16150  ramub2  16947  ressinbas  17177  ressress  17179  submre  17529  mrcss  17544  mreacs  17586  drsdirfi  18233  clatglbss  18447  ipopos  18464  chnrdss  18545  cntz2ss  19269  pgrpsubgsymg  19343  ablfac1eulem  20008  subrngint  20498  subrgint  20533  tgval  22904  mretopd  23041  ssnei  23059  opnneiss  23067  restdis  23127  restcls  23130  restntr  23131  tgcnp  23202  fbssfi  23786  fgss2  23823  fgcl  23827  supfil  23844  alexsubALTlem3  23998  alexsubALTlem4  23999  cnextcn  24016  ustex3sym  24167  trust  24178  restutop  24186  utop2nei  24199  cfiluweak  24243  blssexps  24375  blssex  24376  mopni3  24443  metss  24457  metcnp3  24489  metust  24507  cfilucfil  24508  psmetutop  24516  tgioo  24745  xrsmopn  24762  fsumcn  24822  cncfmptid  24867  iscmet3lem2  25253  caussi  25258  ovolsslem  25446  ovolsscl  25448  ovolssnul  25449  opnmblALT  25565  itgfsum  25789  limcresi  25847  dvmptfsum  25940  plyss  26165  madebdayim  27889  cofcutrtime  27928  n0fincut  28356  nbuhgr  29421  chsupunss  31424  shsupunss  31426  spanss  31428  shslubi  31465  shlub  31494  mdsl1i  32401  mdsl2i  32402  cvmdi  32404  mdslmd1lem1  32405  mdslmd1lem2  32406  mdslmd2i  32410  mdslmd4i  32413  atomli  32462  atcvatlem  32465  chirredlem2  32471  chirredi  32474  mdsymlem5  32487  xrge0infss  32843  tpr2rico  34082  sigainb  34306  dya2icoseg2  34448  omssubadd  34470  eulerpartlemn  34551  ballotlem2  34659  fissorduni  35259  nummin  35262  cvmlift2lem12  35521  opnbnd  36532  fneint  36555  dissneqlem  37558  inunissunidif  37593  pibt2  37635  fin2so  37821  matunitlindflem1  37830  mblfinlem4  37874  ismblfin  37875  filbcmb  37954  heiborlem10  38034  igenmin  38278  lssatle  39354  paddss1  40156  paddss2  40157  paddss12  40158  paddssw2  40183  pclssN  40233  pclfinN  40239  polsubN  40246  2polvalN  40253  2polssN  40254  3polN  40255  2pmaplubN  40265  pnonsingN  40272  polsubclN  40291  dihord6apre  41595  dochsscl  41707  mapdordlem2  41976  isnacs3  43030  itgoss  43483  ofoaid1  43678  ofoaid2  43679  sspwimp  45236  sspwimpVD  45237  nsstr  45417  islptre  45942  gsumlsscl  48703  lincellss  48749  ellcoellss  48758