Theorem sstr 3900

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

Syntax hints:   → wi 4   ∧ wa 399   ⊆ wss 3858

This theorem was proved from axioms:  ax-mp 5  ax-1 6  ax-2 7  ax-3 8  ax-gen 1797  ax-4 1811  ax-5 1911  ax-6 1970  ax-7 2015  ax-8 2113  ax-9 2121  ax-ext 2729

This theorem depends on definitions:  df-bi 210  df-an 400  df-tru 1541  df-ex 1782  df-sb 2070  df-clab 2736  df-cleq 2750  df-clel 2830  df-v 3411  df-in 3865  df-ss 3875

This theorem is referenced by:  sstrd  3902  sylan9ss  3905  ssdifss  4041  uneqin  4183  intss2  4995  ssrnres  6007  relrelss  6102  fco  6516  fssres  6529  ssimaex  6737  dff3  6857  tpostpos2  7923  smores  7999  om00  8211  omeulem2  8219  pmss12g  8451  unblem1  8803  unblem2  8804  unblem3  8805  unblem4  8806  isfinite2  8809  cantnfval2  9165  cantnfle  9167  rankxplim3  9343  alephinit  9555  dfac12lem2  9604  ackbij1lem11  9690  cfeq0  9716  cfsuc  9717  cff1  9718  cflim2  9723  cfss  9725  cfslb2n  9728  cofsmo  9729  cfsmolem  9730  fin23lem34  9806  fin1a2lem13  9872  axdc3lem2  9911  axdclem  9979  pwcfsdom  10043  wunfi  10181  tskxpss  10232  tskcard  10241  suprzcl  12101  uzwo  12351  uzwo2  12352  infssuzle  12371  infssuzcl  12372  supxrbnd  12762  supxrgtmnf  12763  supxrre1  12764  supxrre2  12765  supxrss  12766  infxrss  12773  iccsupr  12874  hashf1lem2  13866  trclun  14421  fsum2d  15174  fsumabs  15204  fsumrlim  15214  fsumo1  15215  fprod2d  15383  rpnnen2lem4  15618  rpnnen2lem7  15621  ramub2  16405  ressinbas  16618  ressress  16620  submre  16934  mrcss  16945  mreacs  16987  drsdirfi  17614  clatglbss  17803  ipopos  17836  cntz2ss  18530  pgrpsubgsymg  18604  ablfac1eulem  19262  subrgint  19625  tgval  21655  mretopd  21792  ssnei  21810  opnneiss  21818  restdis  21878  restcls  21881  restntr  21882  tgcnp  21953  fbssfi  22537  fgss2  22574  fgcl  22578  supfil  22595  alexsubALTlem3  22749  alexsubALTlem4  22750  cnextcn  22767  ustex3sym  22918  trust  22930  restutop  22938  utop2nei  22951  cfiluweak  22996  blssexps  23128  blssex  23129  mopni3  23196  metss  23210  metcnp3  23242  metust  23260  cfilucfil  23261  psmetutop  23269  tgioo  23497  xrsmopn  23513  fsumcn  23571  cncfmptid  23614  iscmet3lem2  23992  caussi  23997  ovolsslem  24184  ovolsscl  24186  ovolssnul  24187  opnmblALT  24303  itgfsum  24526  limcresi  24584  dvmptfsum  24674  plyss  24895  nbuhgr  27232  chsupunss  29226  shsupunss  29228  spanss  29230  shslubi  29267  shlub  29296  mdsl1i  30203  mdsl2i  30204  cvmdi  30206  mdslmd1lem1  30207  mdslmd1lem2  30208  mdslmd2i  30212  mdslmd4i  30215  atomli  30264  atcvatlem  30267  chirredlem2  30273  chirredi  30276  mdsymlem5  30289  xrge0infss  30607  tpr2rico  31383  sigainb  31623  dya2icoseg2  31764  omssubadd  31786  eulerpartlemn  31867  ballotlem2  31974  nummin  32592  cvmlift2lem12  32792  opnbnd  34063  fneint  34086  dissneqlem  35037  inunissunidif  35072  pibt2  35114  fin2so  35324  matunitlindflem1  35333  mblfinlem4  35377  ismblfin  35378  filbcmb  35458  heiborlem10  35538  igenmin  35782  lssatle  36591  paddss1  37393  paddss2  37394  paddss12  37395  paddssw2  37420  pclssN  37470  pclfinN  37476  polsubN  37483  2polvalN  37490  2polssN  37491  3polN  37492  2pmaplubN  37502  pnonsingN  37509  polsubclN  37528  dihord6apre  38832  dochsscl  38944  mapdordlem2  39213  isnacs3  40024  itgoss  40480  sspwimp  41997  sspwimpVD  41998  nsstr  42104  islptre  42627  gsumlsscl  45152  lincellss  45200  ellcoellss  45209