Theorem sstr 3944

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

Syntax hints:   → wi 4   ∧ wa 400   ⊆ wss 3904

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

This theorem depends on definitions:  df-bi 210  df-an 401  df-ss 3921

This theorem is referenced by:  sstrd  3946  sylan9ss  3949  ssdifss  4093  uneqin  4241  intss2  5073  ssrnres  6176  relrelss  6274  fcof  6729  fssres  6744  ssimaex  6966  dff3  7095  tpostpos2  8242  smores  8338  om00  8559  omeulem2  8567  cofonr  8659  naddunif  8679  pmss12g  8866  unblem1  9251  unblem2  9252  unblem3  9253  unblem4  9254  isfinite2  9257  cantnfval2  9637  cantnfle  9639  rankxplim3  9852  alephinit  10078  dfac12lem2  10127  ackbij1lem11  10211  cfeq0  10239  cfsuc  10240  cff1  10241  cflim2  10246  cfss  10248  cfslb2n  10251  cofsmo  10252  cfsmolem  10253  fin23lem34  10329  fin1a2lem13  10395  axdc3lem2  10434  axdclem  10502  pwcfsdom  10567  wunfi  10705  tskxpss  10756  tskcard  10765  suprzcl  12675  uzwo  12934  uzwo2  12935  infssuzle  12954  infssuzcl  12955  supxrbnd  13353  supxrgtmnf  13354  supxrre1  13355  supxrre2  13356  supxrss  13357  infxrss  13365  iccsupr  13468  hashf1lem2  14492  trclun  15050  fsum2d  15821  fsumabs  15852  fsumrlim  15862  fsumo1  15863  fprod2d  16034  rpnnen2lem4  16272  rpnnen2lem7  16275  ramub2  17073  ressinbas  17304  ressress  17306  submre  17656  mrcss  17671  mreacs  17713  drsdirfi  18360  clatglbss  18574  ipopos  18591  chnrdss  18672  cntz2ss  19404  pgrpsubgsymg  19478  ablfac1eulem  20143  subrngint  20644  subrgint  20679  tgval  23091  mretopd  23228  ssnei  23246  opnneiss  23254  restdis  23314  restcls  23317  restntr  23318  tgcnp  23389  fbssfi  23973  fgss2  24010  fgcl  24014  supfil  24031  alexsubALTlem3  24185  alexsubALTlem4  24186  cnextcn  24203  ustex3sym  24354  trust  24365  restutop  24373  utop2nei  24386  cfiluweak  24430  blssexps  24562  blssex  24563  mopni3  24630  metss  24644  metcnp3  24676  metust  24694  cfilucfil  24695  psmetutop  24703  tgioo  24932  xrsmopn  24949  fsumcn  25008  cncfmptid  25051  iscmet3lem2  25430  caussi  25435  ovolsslem  25622  ovolsscl  25624  ovolssnul  25625  opnmblALT  25741  itgfsum  25965  limcresi  26023  dvmptfsum  26113  plyss  26335  madebdayim  28057  cofcutrtime  28096  n0fincut  28524  nbuhgr  29659  chsupunss  31662  shsupunss  31664  spanss  31666  shslubi  31703  shlub  31732  mdsl1i  32639  mdsl2i  32640  cvmdi  32642  mdslmd1lem1  32643  mdslmd1lem2  32644  mdslmd2i  32648  mdslmd4i  32651  atomli  32700  atcvatlem  32703  chirredlem2  32709  chirredi  32712  mdsymlem5  32725  xrge0infss  33071  tpr2rico  34268  sigainb  34492  dya2icoseg2  34634  omssubadd  34656  eulerpartlemn  34737  ballotlem2  34845  fissorduni  35444  nummin  35448  cvmlift2lem12  35760  opnbnd  36780  fneint  36803  ttcss2  36954  ssttctr  36959  dissneqlem  37930  inunissunidif  37965  pibt2  38007  fin2so  38202  matunitlindflem1  38211  mblfinlem4  38255  ismblfin  38256  filbcmb  38335  heiborlem10  38415  igenmin  38659  lssatle  39735  paddss1  40537  paddss2  40538  paddss12  40539  paddssw2  40564  pclssN  40614  pclfinN  40620  polsubN  40627  2polvalN  40634  2polssN  40635  3polN  40636  2pmaplubN  40646  pnonsingN  40653  polsubclN  40672  dihord6apre  41976  dochsscl  42088  mapdordlem2  42357  isnacs3  43389  itgoss  43838  ofoaid1  44033  ofoaid2  44034  sspwimp  45574  sspwimpVD  45575  nsstr  45761  islptre  46283  gsumlsscl  49105  lincellss  49151  ellcoellss  49160