Theorem sstr 3945

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

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

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

This theorem depends on definitions:  df-bi 209  df-an 400  df-ss 3922

This theorem is referenced by:  sstrd  3947  sylan9ss  3950  ssdifss  4094  uneqin  4242  intss2  5066  ssrnres  6164  relrelss  6260  fcof  6715  fssres  6730  ssimaex  6952  dff3  7081  tpostpos2  8227  smores  8323  om00  8544  omeulem2  8552  cofonr  8644  naddunif  8664  pmss12g  8851  unblem1  9236  unblem2  9237  unblem3  9238  unblem4  9239  isfinite2  9242  cantnfval2  9622  cantnfle  9624  rankxplim3  9837  alephinit  10063  dfac12lem2  10112  ackbij1lem11  10196  cfeq0  10224  cfsuc  10225  cff1  10226  cflim2  10231  cfss  10233  cfslb2n  10236  cofsmo  10237  cfsmolem  10238  fin23lem34  10314  fin1a2lem13  10380  axdc3lem2  10419  axdclem  10487  pwcfsdom  10552  wunfi  10690  tskxpss  10741  tskcard  10750  suprzcl  12663  uzwo  12922  uzwo2  12923  infssuzle  12942  infssuzcl  12943  supxrbnd  13341  supxrgtmnf  13342  supxrre1  13343  supxrre2  13344  supxrss  13345  infxrss  13353  iccsupr  13456  hashf1lem2  14479  trclun  15037  fsum2d  15808  fsumabs  15839  fsumrlim  15849  fsumo1  15850  fprod2d  16021  rpnnen2lem4  16259  rpnnen2lem7  16262  ramub2  17060  ressinbas  17291  ressress  17293  submre  17643  mrcss  17658  mreacs  17700  drsdirfi  18347  clatglbss  18561  ipopos  18578  chnrdss  18659  cntz2ss  19385  pgrpsubgsymg  19459  ablfac1eulem  20124  subrngint  20620  subrgint  20655  tgval  23022  mretopd  23159  ssnei  23177  opnneiss  23185  restdis  23245  restcls  23248  restntr  23249  tgcnp  23320  fbssfi  23904  fgss2  23941  fgcl  23945  supfil  23962  alexsubALTlem3  24116  alexsubALTlem4  24117  cnextcn  24134  ustex3sym  24285  trust  24296  restutop  24304  utop2nei  24317  cfiluweak  24361  blssexps  24493  blssex  24494  mopni3  24561  metss  24575  metcnp3  24607  metust  24625  cfilucfil  24626  psmetutop  24634  tgioo  24863  xrsmopn  24880  fsumcn  24939  cncfmptid  24982  iscmet3lem2  25361  caussi  25366  ovolsslem  25553  ovolsscl  25555  ovolssnul  25556  opnmblALT  25672  itgfsum  25896  limcresi  25954  dvmptfsum  26044  plyss  26266  madebdayim  27988  cofcutrtime  28027  n0fincut  28455  nbuhgr  29551  chsupunss  31554  shsupunss  31556  spanss  31558  shslubi  31595  shlub  31624  mdsl1i  32531  mdsl2i  32532  cvmdi  32534  mdslmd1lem1  32535  mdslmd1lem2  32536  mdslmd2i  32540  mdslmd4i  32543  atomli  32592  atcvatlem  32595  chirredlem2  32601  chirredi  32604  mdsymlem5  32617  xrge0infss  32968  tpr2rico  34211  sigainb  34435  dya2icoseg2  34577  omssubadd  34599  eulerpartlemn  34680  ballotlem2  34788  fissorduni  35387  nummin  35391  cvmlift2lem12  35669  opnbnd  36690  fneint  36713  ttcss2  36864  ssttctr  36869  dissneqlem  37839  inunissunidif  37874  pibt2  37916  fin2so  38111  matunitlindflem1  38120  mblfinlem4  38164  ismblfin  38165  filbcmb  38244  heiborlem10  38324  igenmin  38568  lssatle  39644  paddss1  40446  paddss2  40447  paddss12  40448  paddssw2  40473  pclssN  40523  pclfinN  40529  polsubN  40536  2polvalN  40543  2polssN  40544  3polN  40545  2pmaplubN  40555  pnonsingN  40562  polsubclN  40581  dihord6apre  41885  dochsscl  41997  mapdordlem2  42266  isnacs3  43296  itgoss  43745  ofoaid1  43940  ofoaid2  43941  sspwimp  45484  sspwimpVD  45485  nsstr  45664  islptre  46186  gsumlsscl  48993  lincellss  49039  ellcoellss  49048