Theorem sstr 3931

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

Syntax hints:   → wi 4   ∧ wa 395   ⊆ wss 3890

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

This theorem depends on definitions:  df-bi 207  df-an 396  df-ss 3907

This theorem is referenced by:  sstrd  3933  sylan9ss  3936  ssdifss  4081  uneqin  4230  intss2  5051  ssrnres  6143  relrelss  6238  fcof  6692  fssres  6707  ssimaex  6926  dff3  7053  tpostpos2  8197  smores  8292  om00  8510  omeulem2  8518  cofonr  8610  naddunif  8629  pmss12g  8817  unblem1  9202  unblem2  9203  unblem3  9204  unblem4  9205  isfinite2  9208  cantnfval2  9590  cantnfle  9592  rankxplim3  9805  alephinit  10017  dfac12lem2  10067  ackbij1lem11  10151  cfeq0  10178  cfsuc  10179  cff1  10180  cflim2  10185  cfss  10187  cfslb2n  10190  cofsmo  10191  cfsmolem  10192  fin23lem34  10268  fin1a2lem13  10334  axdc3lem2  10373  axdclem  10441  pwcfsdom  10506  wunfi  10644  tskxpss  10695  tskcard  10704  suprzcl  12609  uzwo  12861  uzwo2  12862  infssuzle  12881  infssuzcl  12882  supxrbnd  13280  supxrgtmnf  13281  supxrre1  13282  supxrre2  13283  supxrss  13284  infxrss  13292  iccsupr  13395  hashf1lem2  14418  trclun  14976  fsum2d  15733  fsumabs  15764  fsumrlim  15774  fsumo1  15775  fprod2d  15946  rpnnen2lem4  16184  rpnnen2lem7  16187  ramub2  16985  ressinbas  17215  ressress  17217  submre  17567  mrcss  17582  mreacs  17624  drsdirfi  18271  clatglbss  18485  ipopos  18502  chnrdss  18583  cntz2ss  19310  pgrpsubgsymg  19384  ablfac1eulem  20049  subrngint  20537  subrgint  20572  tgval  22920  mretopd  23057  ssnei  23075  opnneiss  23083  restdis  23143  restcls  23146  restntr  23147  tgcnp  23218  fbssfi  23802  fgss2  23839  fgcl  23843  supfil  23860  alexsubALTlem3  24014  alexsubALTlem4  24015  cnextcn  24032  ustex3sym  24183  trust  24194  restutop  24202  utop2nei  24215  cfiluweak  24259  blssexps  24391  blssex  24392  mopni3  24459  metss  24473  metcnp3  24505  metust  24523  cfilucfil  24524  psmetutop  24532  tgioo  24761  xrsmopn  24778  fsumcn  24837  cncfmptid  24880  iscmet3lem2  25259  caussi  25264  ovolsslem  25451  ovolsscl  25453  ovolssnul  25454  opnmblALT  25570  itgfsum  25794  limcresi  25852  dvmptfsum  25942  plyss  26164  madebdayim  27880  cofcutrtime  27919  n0fincut  28347  nbuhgr  29412  chsupunss  31415  shsupunss  31417  spanss  31419  shslubi  31456  shlub  31485  mdsl1i  32392  mdsl2i  32393  cvmdi  32395  mdslmd1lem1  32396  mdslmd1lem2  32397  mdslmd2i  32401  mdslmd4i  32404  atomli  32453  atcvatlem  32456  chirredlem2  32462  chirredi  32465  mdsymlem5  32478  xrge0infss  32833  tpr2rico  34056  sigainb  34280  dya2icoseg2  34422  omssubadd  34444  eulerpartlemn  34525  ballotlem2  34633  fissorduni  35233  nummin  35236  cvmlift2lem12  35496  opnbnd  36507  fneint  36530  ttcss2  36681  ssttctr  36686  dissneqlem  37656  inunissunidif  37691  pibt2  37733  fin2so  37928  matunitlindflem1  37937  mblfinlem4  37981  ismblfin  37982  filbcmb  38061  heiborlem10  38141  igenmin  38385  lssatle  39461  paddss1  40263  paddss2  40264  paddss12  40265  paddssw2  40290  pclssN  40340  pclfinN  40346  polsubN  40353  2polvalN  40360  2polssN  40361  3polN  40362  2pmaplubN  40372  pnonsingN  40379  polsubclN  40398  dihord6apre  41702  dochsscl  41814  mapdordlem2  42083  isnacs3  43142  itgoss  43591  ofoaid1  43786  ofoaid2  43787  sspwimp  45344  sspwimpVD  45345  nsstr  45525  islptre  46049  gsumlsscl  48850  lincellss  48896  ellcoellss  48905