Theorem sstr 3925

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

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

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 3902

This theorem is referenced by:  sstrd  3927  sylan9ss  3930  ssdifss  4072  uneqin  4219  intss2  5039  ssrnres  6131  relrelss  6226  fcof  6680  fssres  6695  ssimaex  6914  dff3  7041  tpostpos2  8186  smores  8281  om00  8499  omeulem2  8507  cofonr  8599  naddunif  8618  pmss12g  8806  unblem1  9191  unblem2  9192  unblem3  9193  unblem4  9194  isfinite2  9197  cantnfval2  9579  cantnfle  9581  rankxplim3  9794  alephinit  10006  dfac12lem2  10056  ackbij1lem11  10140  cfeq0  10167  cfsuc  10168  cff1  10169  cflim2  10174  cfss  10176  cfslb2n  10179  cofsmo  10180  cfsmolem  10181  fin23lem34  10257  fin1a2lem13  10323  axdc3lem2  10362  axdclem  10430  pwcfsdom  10495  wunfi  10633  tskxpss  10684  tskcard  10693  suprzcl  12598  uzwo  12850  uzwo2  12851  infssuzle  12870  infssuzcl  12871  supxrbnd  13269  supxrgtmnf  13270  supxrre1  13271  supxrre2  13272  supxrss  13273  infxrss  13281  iccsupr  13384  hashf1lem2  14407  trclun  14965  fsum2d  15722  fsumabs  15753  fsumrlim  15763  fsumo1  15764  fprod2d  15935  rpnnen2lem4  16173  rpnnen2lem7  16176  ramub2  16974  ressinbas  17204  ressress  17206  submre  17556  mrcss  17571  mreacs  17613  drsdirfi  18260  clatglbss  18474  ipopos  18491  chnrdss  18572  cntz2ss  19299  pgrpsubgsymg  19373  ablfac1eulem  20038  subrngint  20526  subrgint  20561  tgval  22908  mretopd  23045  ssnei  23063  opnneiss  23071  restdis  23131  restcls  23134  restntr  23135  tgcnp  23206  fbssfi  23790  fgss2  23827  fgcl  23831  supfil  23848  alexsubALTlem3  24002  alexsubALTlem4  24003  cnextcn  24020  ustex3sym  24171  trust  24182  restutop  24190  utop2nei  24203  cfiluweak  24247  blssexps  24379  blssex  24380  mopni3  24447  metss  24461  metcnp3  24493  metust  24511  cfilucfil  24512  psmetutop  24520  tgioo  24749  xrsmopn  24766  fsumcn  24825  cncfmptid  24868  iscmet3lem2  25247  caussi  25252  ovolsslem  25439  ovolsscl  25441  ovolssnul  25442  opnmblALT  25558  itgfsum  25782  limcresi  25840  dvmptfsum  25930  plyss  26152  madebdayim  27868  cofcutrtime  27907  n0fincut  28335  nbuhgr  29400  chsupunss  31403  shsupunss  31405  spanss  31407  shslubi  31444  shlub  31473  mdsl1i  32380  mdsl2i  32381  cvmdi  32383  mdslmd1lem1  32384  mdslmd1lem2  32385  mdslmd2i  32389  mdslmd4i  32392  atomli  32441  atcvatlem  32444  chirredlem2  32450  chirredi  32453  mdsymlem5  32466  xrge0infss  32821  tpr2rico  34044  sigainb  34268  dya2icoseg2  34410  omssubadd  34432  eulerpartlemn  34513  ballotlem2  34621  fissorduni  35221  nummin  35224  cvmlift2lem12  35484  opnbnd  36495  fneint  36518  ttcss2  36669  ssttctr  36674  dissneqlem  37644  inunissunidif  37679  pibt2  37721  fin2so  37916  matunitlindflem1  37925  mblfinlem4  37969  ismblfin  37970  filbcmb  38049  heiborlem10  38129  igenmin  38373  lssatle  39449  paddss1  40251  paddss2  40252  paddss12  40253  paddssw2  40278  pclssN  40328  pclfinN  40334  polsubN  40341  2polvalN  40348  2polssN  40349  3polN  40350  2pmaplubN  40360  pnonsingN  40367  polsubclN  40386  dihord6apre  41690  dochsscl  41802  mapdordlem2  42071  isnacs3  43130  itgoss  43579  ofoaid1  43774  ofoaid2  43775  sspwimp  45332  sspwimpVD  45333  nsstr  45513  islptre  46037  gsumlsscl  48844  lincellss  48890  ellcoellss  48899