Theorem sstr 3921

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

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

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 3901

This theorem is used by:  sstrd  3923  sylan9ss  3926  ssdifss  4079  uneqin  4237  intss2  5071  ssrnres  6182  relrelss  6293  fcof  6755  fssres  6770  ssimaex  6993  dff3  7124  tpostpos2  8292  smores  8388  om00  8611  omeulem2  8619  cofonr  8711  naddunif  8731  pmss12g  8925  fissorduni  9310  unblem1  9312  unblem2  9313  unblem3  9314  unblem4  9315  isfinite2  9318  cantnfval2  9697  cantnfle  9699  rankxplim3  9925  hfsshf  9942  hfuni  9951  alephinit  10201  dfac12lem2  10250  ackbij1lem11  10334  cfeq0  10361  cfsuc  10362  cff1  10363  cflim2  10368  cfss  10370  cfslb2n  10373  cofsmo  10374  cfsmolem  10375  fin23lem34  10451  fin1a2lem13  10517  axdc3lem2  10556  axdclem  10624  pwcfsdom  10695  wunfi  10833  tskxpss  10884  tskcard  10893  suprzcl  12806  uzwo  13065  uzwo2  13066  infssuzle  13085  infssuzcl  13086  supxrbnd  13485  supxrgtmnf  13486  supxrre1  13487  supxrre2  13488  supxrss  13489  infxrss  13497  iccsupr  13600  hashf1lem2  14628  trclun  15196  fsum2d  15966  fsumabs  15997  fsumrlim  16007  fsumo1  16008  fprod2d  16177  rpnnen2lem4  16414  rpnnen2lem7  16417  ramub2  17221  ressinbas  17452  ressress  17454  submre  17804  mrcss  17819  mreacs  17861  drsdirfi  18508  clatglbss  18722  ipopos  18739  chnrdss  18820  cntz2ss  19579  pgrpsubgsymg  19653  ablfac1eulem  20318  subrngint  20842  subrgint  20877  matunitlindflem1  23024  tgval  23303  mretopd  23440  ssnei  23458  opnneiss  23466  restdis  23526  restcls  23529  restntr  23530  tgcnp  23601  fbssfi  24186  fgss2  24223  fgcl  24227  supfil  24244  alexsubALTlem3  24398  alexsubALTlem4  24399  cnextcn  24416  ustex3sym  24567  trust  24578  restutop  24586  utop2nei  24599  cfiluweak  24643  blssexps  24775  blssex  24776  mopni3  24843  metss  24857  metcnp3  24889  metust  24907  cfilucfil  24908  psmetutop  24916  tgioo  25145  xrsmopn  25162  fsumcn  25221  cncfmptid  25264  iscmet3lem2  25643  caussi  25648  ovolsslem  25835  ovolsscl  25837  ovolssnul  25838  opnmblALT  25954  itgfsum  26177  limcresi  26235  dvmptfsum  26325  plyss  26547  madebdayim  28304  cofcutrtime  28343  n0fincut  28771  nbuhgr  29954  chsupunss  31976  shsupunss  31978  spanss  31980  shslubi  32017  shlub  32046  mdsl1i  32953  mdsl2i  32954  cvmdi  32956  mdslmd1lem1  32957  mdslmd1lem2  32958  mdslmd2i  32962  mdslmd4i  32965  atomli  33014  atcvatlem  33017  chirredlem2  33023  chirredi  33026  mdsymlem5  33039  xrge0infss  33422  tpr2rico  34614  sigainb  34839  dya2icoseg2  34980  omssubadd  35002  eulerpartlemn  35083  ballotlem2  35191  nummin  35806  cvmlift2lem12  36246  opnbnd  37291  fneint  37314  ttcss2  37465  ssttctr  37470  dissneqlem  38455  inunissunidif  38490  pibt2  38532  fin2so  38722  mblfinlem4  38770  ismblfin  38771  filbcmb  38866  heiborlem10  38946  igenmin  39190  lssatle  40264  paddss1  41066  paddss2  41067  paddss12  41068  paddssw2  41093  pclssN  41143  pclfinN  41149  polsubN  41156  2polvalN  41163  2polssN  41164  3polN  41165  2pmaplubN  41175  pnonsingN  41182  polsubclN  41201  dihord6apre  42505  dochsscl  42617  mapdordlem2  42886  isnacs3  43914  itgoss  44357  ofoaid1  44552  ofoaid2  44553  sspwimp  46091  sspwimpVD  46092  nsstr  46315  islptre  46836  gsumlsscl  49697  lincellss  49743  ellcoellss  49752