Theorem sstr 3942

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

This proof depends on syntax axioms:   → wi 4   ∧ wa 401   ⊆ wss 3902

This proof depends on axioms:  ax-mp 5  ax-1 6  ax-2 7  ax-3 8  ax-gen 1828  ax-4 1842

This proof depends on definitions:  df-bi 210  df-an 402  df-ss 3919

This theorem is used by:  sstrd  3944  sylan9ss  3947  ssdifss  4090  uneqin  4238  intss2  5072  ssrnres  6175  relrelss  6274  fcof  6730  fssres  6745  ssimaex  6967  dff3  7096  tpostpos2  8248  smores  8344  om00  8565  omeulem2  8573  cofonr  8665  naddunif  8685  pmss12g  8879  unblem1  9265  unblem2  9266  unblem3  9267  unblem4  9268  isfinite2  9271  cantnfval2  9651  cantnfle  9653  rankxplim3  9866  alephinit  10101  dfac12lem2  10150  ackbij1lem11  10234  cfeq0  10261  cfsuc  10262  cff1  10263  cflim2  10268  cfss  10270  cfslb2n  10273  cofsmo  10274  cfsmolem  10275  fin23lem34  10351  fin1a2lem13  10417  axdc3lem2  10456  axdclem  10524  pwcfsdom  10595  wunfi  10733  tskxpss  10784  tskcard  10793  suprzcl  12704  uzwo  12963  uzwo2  12964  infssuzle  12983  infssuzcl  12984  supxrbnd  13382  supxrgtmnf  13383  supxrre1  13384  supxrre2  13385  supxrss  13386  infxrss  13394  iccsupr  13497  hashf1lem2  14523  trclun  15089  fsum2d  15859  fsumabs  15890  fsumrlim  15900  fsumo1  15901  fprod2d  16072  rpnnen2lem4  16309  rpnnen2lem7  16312  ramub2  17110  ressinbas  17341  ressress  17343  submre  17693  mrcss  17708  mreacs  17750  drsdirfi  18397  clatglbss  18611  ipopos  18628  chnrdss  18709  cntz2ss  19463  pgrpsubgsymg  19537  ablfac1eulem  20202  subrngint  20723  subrgint  20758  matunitlindflem1  22902  tgval  23181  mretopd  23318  ssnei  23336  opnneiss  23344  restdis  23404  restcls  23407  restntr  23408  tgcnp  23479  fbssfi  24064  fgss2  24101  fgcl  24105  supfil  24122  alexsubALTlem3  24276  alexsubALTlem4  24277  cnextcn  24294  ustex3sym  24445  trust  24456  restutop  24464  utop2nei  24477  cfiluweak  24521  blssexps  24653  blssex  24654  mopni3  24721  metss  24735  metcnp3  24767  metust  24785  cfilucfil  24786  psmetutop  24794  tgioo  25023  xrsmopn  25040  fsumcn  25099  cncfmptid  25142  iscmet3lem2  25521  caussi  25526  ovolsslem  25713  ovolsscl  25715  ovolssnul  25716  opnmblALT  25832  itgfsum  26056  limcresi  26114  dvmptfsum  26204  plyss  26426  madebdayim  28151  cofcutrtime  28190  n0fincut  28618  nbuhgr  29789  chsupunss  31811  shsupunss  31813  spanss  31815  shslubi  31852  shlub  31881  mdsl1i  32788  mdsl2i  32789  cvmdi  32791  mdslmd1lem1  32792  mdslmd1lem2  32793  mdslmd2i  32797  mdslmd4i  32800  atomli  32849  atcvatlem  32852  chirredlem2  32858  chirredi  32861  mdsymlem5  32874  xrge0infss  33218  tpr2rico  34409  sigainb  34634  dya2icoseg2  34776  omssubadd  34798  eulerpartlemn  34879  ballotlem2  34987  fissorduni  35581  nummin  35585  cvmlift2lem12  35880  opnbnd  36931  fneint  36954  ttcss2  37105  ssttctr  37110  dissneqlem  38081  inunissunidif  38116  pibt2  38158  fin2so  38348  mblfinlem4  38396  ismblfin  38397  filbcmb  38477  heiborlem10  38557  igenmin  38801  lssatle  39875  paddss1  40677  paddss2  40678  paddss12  40679  paddssw2  40704  pclssN  40754  pclfinN  40760  polsubN  40767  2polvalN  40774  2polssN  40775  3polN  40776  2pmaplubN  40786  pnonsingN  40793  polsubclN  40812  dihord6apre  42116  dochsscl  42228  mapdordlem2  42497  isnacs3  43542  itgoss  43991  ofoaid1  44186  ofoaid2  44187  sspwimp  45727  sspwimpVD  45728  nsstr  45914  islptre  46436  gsumlsscl  49297  lincellss  49343  ellcoellss  49352