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 ⊢ ((𝐴 ⊆ 𝐵 ∧ 𝐵 ⊆ 𝐶) → 𝐴 ⊆ 𝐶)

This proof depends on syntax axioms:   → wi 4   ∧ wa 400   ⊆ wss 3904

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

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

This theorem is used by:  sstrd  3946  sylan9ss  3949  ssdifss  4093  uneqin  4241  intss2  5073  ssrnres  6175  relrelss  6274  fcof  6729  fssres  6744  ssimaex  6966  dff3  7095  tpostpos2  8241  smores  8337  om00  8558  omeulem2  8566  cofonr  8658  naddunif  8678  pmss12g  8865  unblem1  9250  unblem2  9251  unblem3  9252  unblem4  9253  isfinite2  9256  cantnfval2  9636  cantnfle  9638  rankxplim3  9851  alephinit  10086  dfac12lem2  10135  ackbij1lem11  10219  cfeq0  10246  cfsuc  10247  cff1  10248  cflim2  10253  cfss  10255  cfslb2n  10258  cofsmo  10259  cfsmolem  10260  fin23lem34  10336  fin1a2lem13  10402  axdc3lem2  10441  axdclem  10509  pwcfsdom  10574  wunfi  10712  tskxpss  10763  tskcard  10772  suprzcl  12682  uzwo  12941  uzwo2  12942  infssuzle  12961  infssuzcl  12962  supxrbnd  13360  supxrgtmnf  13361  supxrre1  13362  supxrre2  13363  supxrss  13364  infxrss  13372  iccsupr  13475  hashf1lem2  14500  trclun  15058  fsum2d  15829  fsumabs  15860  fsumrlim  15870  fsumo1  15871  fprod2d  16042  rpnnen2lem4  16279  rpnnen2lem7  16282  ramub2  17080  ressinbas  17311  ressress  17313  submre  17663  mrcss  17678  mreacs  17720  drsdirfi  18367  clatglbss  18581  ipopos  18598  chnrdss  18679  cntz2ss  19411  pgrpsubgsymg  19485  ablfac1eulem  20150  subrngint  20670  subrgint  20705  tgval  23123  mretopd  23260  ssnei  23278  opnneiss  23286  restdis  23346  restcls  23349  restntr  23350  tgcnp  23421  fbssfi  24005  fgss2  24042  fgcl  24046  supfil  24063  alexsubALTlem3  24217  alexsubALTlem4  24218  cnextcn  24235  ustex3sym  24386  trust  24397  restutop  24405  utop2nei  24418  cfiluweak  24462  blssexps  24594  blssex  24595  mopni3  24662  metss  24676  metcnp3  24708  metust  24726  cfilucfil  24727  psmetutop  24735  tgioo  24964  xrsmopn  24981  fsumcn  25040  cncfmptid  25083  iscmet3lem2  25462  caussi  25467  ovolsslem  25654  ovolsscl  25656  ovolssnul  25657  opnmblALT  25773  itgfsum  25997  limcresi  26055  dvmptfsum  26145  plyss  26367  madebdayim  28092  cofcutrtime  28131  n0fincut  28559  nbuhgr  29704  chsupunss  31707  shsupunss  31709  spanss  31711  shslubi  31748  shlub  31777  mdsl1i  32684  mdsl2i  32685  cvmdi  32687  mdslmd1lem1  32688  mdslmd1lem2  32689  mdslmd2i  32693  mdslmd4i  32696  atomli  32745  atcvatlem  32748  chirredlem2  32754  chirredi  32757  mdsymlem5  32770  xrge0infss  33116  tpr2rico  34311  sigainb  34535  dya2icoseg2  34677  omssubadd  34699  eulerpartlemn  34780  ballotlem2  34888  fissorduni  35489  nummin  35493  cvmlift2lem12  35814  opnbnd  36864  fneint  36887  ttcss2  37038  ssttctr  37043  dissneqlem  38014  inunissunidif  38049  pibt2  38091  fin2so  38286  matunitlindflem1  38295  mblfinlem4  38339  ismblfin  38340  filbcmb  38419  heiborlem10  38499  igenmin  38743  lssatle  39817  paddss1  40619  paddss2  40620  paddss12  40621  paddssw2  40646  pclssN  40696  pclfinN  40702  polsubN  40709  2polvalN  40716  2polssN  40717  3polN  40718  2pmaplubN  40728  pnonsingN  40735  polsubclN  40754  dihord6apre  42058  dochsscl  42170  mapdordlem2  42439  isnacs3  43469  itgoss  43918  ofoaid1  44113  ofoaid2  44114  sspwimp  45654  sspwimpVD  45655  nsstr  45841  islptre  46363  gsumlsscl  49188  lincellss  49234  ellcoellss  49243