Theorem sstr 3938

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

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

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

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

This theorem is referenced by:  sstrd  3940  sylan9ss  3943  ssdifss  4089  uneqin  4238  intss2  5058  ssrnres  6131  relrelss  6226  fcof  6680  fssres  6695  ssimaex  6913  dff3  7039  tpostpos2  8183  smores  8278  om00  8496  omeulem2  8504  cofonr  8595  naddunif  8614  pmss12g  8799  unblem1  9182  unblem2  9183  unblem3  9184  unblem4  9185  isfinite2  9188  cantnfval2  9565  cantnfle  9567  rankxplim3  9780  alephinit  9992  dfac12lem2  10042  ackbij1lem11  10126  cfeq0  10153  cfsuc  10154  cff1  10155  cflim2  10160  cfss  10162  cfslb2n  10165  cofsmo  10166  cfsmolem  10167  fin23lem34  10243  fin1a2lem13  10309  axdc3lem2  10348  axdclem  10416  pwcfsdom  10480  wunfi  10618  tskxpss  10669  tskcard  10678  suprzcl  12559  uzwo  12815  uzwo2  12816  infssuzle  12835  infssuzcl  12836  supxrbnd  13233  supxrgtmnf  13234  supxrre1  13235  supxrre2  13236  supxrss  13237  infxrss  13245  iccsupr  13348  hashf1lem2  14369  trclun  14927  fsum2d  15684  fsumabs  15714  fsumrlim  15724  fsumo1  15725  fprod2d  15894  rpnnen2lem4  16132  rpnnen2lem7  16135  ramub2  16932  ressinbas  17162  ressress  17164  submre  17513  mrcss  17528  mreacs  17570  drsdirfi  18217  clatglbss  18431  ipopos  18448  chnrdss  18529  cntz2ss  19253  pgrpsubgsymg  19327  ablfac1eulem  19992  subrngint  20481  subrgint  20516  tgval  22876  mretopd  23013  ssnei  23031  opnneiss  23039  restdis  23099  restcls  23102  restntr  23103  tgcnp  23174  fbssfi  23758  fgss2  23795  fgcl  23799  supfil  23816  alexsubALTlem3  23970  alexsubALTlem4  23971  cnextcn  23988  ustex3sym  24139  trust  24150  restutop  24158  utop2nei  24171  cfiluweak  24215  blssexps  24347  blssex  24348  mopni3  24415  metss  24429  metcnp3  24461  metust  24479  cfilucfil  24480  psmetutop  24488  tgioo  24717  xrsmopn  24734  fsumcn  24794  cncfmptid  24839  iscmet3lem2  25225  caussi  25230  ovolsslem  25418  ovolsscl  25420  ovolssnul  25421  opnmblALT  25537  itgfsum  25761  limcresi  25819  dvmptfsum  25912  plyss  26137  madebdayim  27839  cofcutrtime  27877  n0sfincut  28288  nbuhgr  29328  chsupunss  31331  shsupunss  31333  spanss  31335  shslubi  31372  shlub  31401  mdsl1i  32308  mdsl2i  32309  cvmdi  32311  mdslmd1lem1  32312  mdslmd1lem2  32313  mdslmd2i  32317  mdslmd4i  32320  atomli  32369  atcvatlem  32372  chirredlem2  32378  chirredi  32381  mdsymlem5  32394  xrge0infss  32750  tpr2rico  33932  sigainb  34156  dya2icoseg2  34298  omssubadd  34320  eulerpartlemn  34401  ballotlem2  34509  fissorduni  35108  nummin  35111  cvmlift2lem12  35365  opnbnd  36376  fneint  36399  dissneqlem  37391  inunissunidif  37426  pibt2  37468  fin2so  37653  matunitlindflem1  37662  mblfinlem4  37706  ismblfin  37707  filbcmb  37786  heiborlem10  37866  igenmin  38110  lssatle  39120  paddss1  39922  paddss2  39923  paddss12  39924  paddssw2  39949  pclssN  39999  pclfinN  40005  polsubN  40012  2polvalN  40019  2polssN  40020  3polN  40021  2pmaplubN  40031  pnonsingN  40038  polsubclN  40057  dihord6apre  41361  dochsscl  41473  mapdordlem2  41742  isnacs3  42808  itgoss  43261  ofoaid1  43456  ofoaid2  43457  sspwimp  45015  sspwimpVD  45016  nsstr  45197  islptre  45724  gsumlsscl  48485  lincellss  48532  ellcoellss  48541