Theorem sstr 3991

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 408	1 ⊢ ((𝐴 ⊆ 𝐵 ∧ 𝐵 ⊆ 𝐶) → 𝐴 ⊆ 𝐶)

Syntax hints:   → wi 4   ∧ wa 397   ⊆ wss 3949

This theorem was proved from axioms:  ax-mp 5  ax-1 6  ax-2 7  ax-3 8  ax-gen 1798  ax-4 1812  ax-5 1914  ax-6 1972  ax-7 2012  ax-8 2109  ax-9 2117  ax-ext 2704

This theorem depends on definitions:  df-bi 206  df-an 398  df-tru 1545  df-ex 1783  df-sb 2069  df-clab 2711  df-cleq 2725  df-clel 2811  df-v 3477  df-in 3956  df-ss 3966

This theorem is referenced by:  sstrd  3993  sylan9ss  3996  ssdifss  4136  uneqin  4279  intss2  5112  ssrnres  6178  relrelss  6273  fcof  6741  fcoOLD  6743  fssres  6758  ssimaex  6977  dff3  7102  tpostpos2  8232  smores  8352  om00  8575  omeulem2  8583  cofonr  8673  naddunif  8692  pmss12g  8863  unblem1  9295  unblem2  9296  unblem3  9297  unblem4  9298  isfinite2  9301  cantnfval2  9664  cantnfle  9666  rankxplim3  9876  alephinit  10090  dfac12lem2  10139  ackbij1lem11  10225  cfeq0  10251  cfsuc  10252  cff1  10253  cflim2  10258  cfss  10260  cfslb2n  10263  cofsmo  10264  cfsmolem  10265  fin23lem34  10341  fin1a2lem13  10407  axdc3lem2  10446  axdclem  10514  pwcfsdom  10578  wunfi  10716  tskxpss  10767  tskcard  10776  suprzcl  12642  uzwo  12895  uzwo2  12896  infssuzle  12915  infssuzcl  12916  supxrbnd  13307  supxrgtmnf  13308  supxrre1  13309  supxrre2  13310  supxrss  13311  infxrss  13318  iccsupr  13419  hashf1lem2  14417  trclun  14961  fsum2d  15717  fsumabs  15747  fsumrlim  15757  fsumo1  15758  fprod2d  15925  rpnnen2lem4  16160  rpnnen2lem7  16163  ramub2  16947  ressinbas  17190  ressress  17193  submre  17549  mrcss  17560  mreacs  17602  drsdirfi  18258  clatglbss  18472  ipopos  18489  cntz2ss  19199  pgrpsubgsymg  19277  ablfac1eulem  19942  subrgint  20342  tgval  22458  mretopd  22596  ssnei  22614  opnneiss  22622  restdis  22682  restcls  22685  restntr  22686  tgcnp  22757  fbssfi  23341  fgss2  23378  fgcl  23382  supfil  23399  alexsubALTlem3  23553  alexsubALTlem4  23554  cnextcn  23571  ustex3sym  23722  trust  23734  restutop  23742  utop2nei  23755  cfiluweak  23800  blssexps  23932  blssex  23933  mopni3  24003  metss  24017  metcnp3  24049  metust  24067  cfilucfil  24068  psmetutop  24076  tgioo  24312  xrsmopn  24328  fsumcn  24386  cncfmptid  24429  iscmet3lem2  24809  caussi  24814  ovolsslem  25001  ovolsscl  25003  ovolssnul  25004  opnmblALT  25120  itgfsum  25344  limcresi  25402  dvmptfsum  25492  plyss  25713  madebdayim  27382  cofcutrtime  27414  nbuhgr  28600  chsupunss  30597  shsupunss  30599  spanss  30601  shslubi  30638  shlub  30667  mdsl1i  31574  mdsl2i  31575  cvmdi  31577  mdslmd1lem1  31578  mdslmd1lem2  31579  mdslmd2i  31583  mdslmd4i  31586  atomli  31635  atcvatlem  31638  chirredlem2  31644  chirredi  31647  mdsymlem5  31660  xrge0infss  31973  tpr2rico  32892  sigainb  33134  dya2icoseg2  33277  omssubadd  33299  eulerpartlemn  33380  ballotlem2  33487  nummin  34094  cvmlift2lem12  34305  opnbnd  35210  fneint  35233  dissneqlem  36221  inunissunidif  36256  pibt2  36298  fin2so  36475  matunitlindflem1  36484  mblfinlem4  36528  ismblfin  36529  filbcmb  36608  heiborlem10  36688  igenmin  36932  lssatle  37885  paddss1  38688  paddss2  38689  paddss12  38690  paddssw2  38715  pclssN  38765  pclfinN  38771  polsubN  38778  2polvalN  38785  2polssN  38786  3polN  38787  2pmaplubN  38797  pnonsingN  38804  polsubclN  38823  dihord6apre  40127  dochsscl  40239  mapdordlem2  40508  isnacs3  41448  itgoss  41905  ofoaid1  42108  ofoaid2  42109  sspwimp  43679  sspwimpVD  43680  nsstr  43784  islptre  44335  subrngint  46739  gsumlsscl  47059  lincellss  47107  ellcoellss  47116