Theorem sstr 3916

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

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

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

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

This theorem is used by:  sstrd  3918  sylan9ss  3921  ssdifss  4076  uneqin  4234  intss2  5067  ssrnres  6169  relrelss  6275  fcof  6733  fssres  6748  ssimaex  6970  dff3  7100  tpostpos2  8264  smores  8360  om00  8583  omeulem2  8591  cofonr  8683  naddunif  8703  pmss12g  8897  fissorduni  9282  unblem1  9284  unblem2  9285  unblem3  9286  unblem4  9287  isfinite2  9290  cantnfval2  9670  cantnfle  9672  rankxplim3  9898  hfsshf  9915  hfuni  9924  alephinit  10174  dfac12lem2  10223  ackbij1lem11  10307  cfeq0  10334  cfsuc  10335  cff1  10336  cflim2  10341  cfss  10343  cfslb2n  10346  cofsmo  10347  cfsmolem  10348  fin23lem34  10424  fin1a2lem13  10490  axdc3lem2  10529  axdclem  10597  pwcfsdom  10668  wunfi  10806  tskxpss  10857  tskcard  10866  suprzcl  12779  uzwo  13038  uzwo2  13039  infssuzle  13058  infssuzcl  13059  supxrbnd  13458  supxrgtmnf  13459  supxrre1  13460  supxrre2  13461  supxrss  13462  infxrss  13470  iccsupr  13573  hashf1lem2  14601  trclun  15167  fsum2d  15937  fsumabs  15968  fsumrlim  15978  fsumo1  15979  fprod2d  16148  rpnnen2lem4  16385  rpnnen2lem7  16388  ramub2  17192  ressinbas  17423  ressress  17425  submre  17775  mrcss  17790  mreacs  17832  drsdirfi  18479  clatglbss  18693  ipopos  18710  chnrdss  18791  cntz2ss  19549  pgrpsubgsymg  19623  ablfac1eulem  20288  subrngint  20812  subrgint  20847  matunitlindflem1  22994  tgval  23273  mretopd  23410  ssnei  23428  opnneiss  23436  restdis  23496  restcls  23499  restntr  23500  tgcnp  23571  fbssfi  24156  fgss2  24193  fgcl  24197  supfil  24214  alexsubALTlem3  24368  alexsubALTlem4  24369  cnextcn  24386  ustex3sym  24537  trust  24548  restutop  24556  utop2nei  24569  cfiluweak  24613  blssexps  24745  blssex  24746  mopni3  24813  metss  24827  metcnp3  24859  metust  24877  cfilucfil  24878  psmetutop  24886  tgioo  25115  xrsmopn  25132  fsumcn  25191  cncfmptid  25234  iscmet3lem2  25613  caussi  25618  ovolsslem  25805  ovolsscl  25807  ovolssnul  25808  opnmblALT  25924  itgfsum  26147  limcresi  26205  dvmptfsum  26295  plyss  26517  madebdayim  28274  cofcutrtime  28313  n0fincut  28741  nbuhgr  29924  chsupunss  31946  shsupunss  31948  spanss  31950  shslubi  31987  shlub  32016  mdsl1i  32923  mdsl2i  32924  cvmdi  32926  mdslmd1lem1  32927  mdslmd1lem2  32928  mdslmd2i  32932  mdslmd4i  32935  atomli  32984  atcvatlem  32987  chirredlem2  32993  chirredi  32996  mdsymlem5  33009  xrge0infss  33394  tpr2rico  34586  sigainb  34811  dya2icoseg2  34952  omssubadd  34974  eulerpartlemn  35055  ballotlem2  35163  nummin  35764  cvmlift2lem12  36121  opnbnd  37155  fneint  37178  ttcss2  37329  ssttctr  37334  dissneqlem  38306  inunissunidif  38341  pibt2  38383  fin2so  38573  mblfinlem4  38621  ismblfin  38622  filbcmb  38717  heiborlem10  38797  igenmin  39041  lssatle  40115  paddss1  40917  paddss2  40918  paddss12  40919  paddssw2  40944  pclssN  40994  pclfinN  41000  polsubN  41007  2polvalN  41014  2polssN  41015  3polN  41016  2pmaplubN  41026  pnonsingN  41033  polsubclN  41052  dihord6apre  42356  dochsscl  42468  mapdordlem2  42737  isnacs3  43764  itgoss  44208  ofoaid1  44403  ofoaid2  44404  sspwimp  45943  sspwimpVD  45944  nsstr  46153  islptre  46674  gsumlsscl  49535  lincellss  49581  ellcoellss  49590