Theorem sstr 3986

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

Syntax hints:   → wi 4   ∧ wa 396   ⊆ wss 3944

This theorem was proved from axioms:  ax-mp 5  ax-1 6  ax-2 7  ax-3 8  ax-gen 1797  ax-4 1811  ax-5 1913  ax-6 1971  ax-7 2011  ax-8 2108  ax-9 2116  ax-ext 2702

This theorem depends on definitions:  df-bi 206  df-an 397  df-tru 1544  df-ex 1782  df-sb 2068  df-clab 2709  df-cleq 2723  df-clel 2809  df-v 3475  df-in 3951  df-ss 3961

This theorem is referenced by:  sstrd  3988  sylan9ss  3991  ssdifss  4131  uneqin  4274  intss2  5104  ssrnres  6166  relrelss  6261  fcof  6727  fcoOLD  6729  fssres  6744  ssimaex  6962  dff3  7086  tpostpos2  8214  smores  8334  om00  8558  omeulem2  8566  cofonr  8656  naddunif  8675  pmss12g  8846  unblem1  9278  unblem2  9279  unblem3  9280  unblem4  9281  isfinite2  9284  cantnfval2  9646  cantnfle  9648  rankxplim3  9858  alephinit  10072  dfac12lem2  10121  ackbij1lem11  10207  cfeq0  10233  cfsuc  10234  cff1  10235  cflim2  10240  cfss  10242  cfslb2n  10245  cofsmo  10246  cfsmolem  10247  fin23lem34  10323  fin1a2lem13  10389  axdc3lem2  10428  axdclem  10496  pwcfsdom  10560  wunfi  10698  tskxpss  10749  tskcard  10758  suprzcl  12624  uzwo  12877  uzwo2  12878  infssuzle  12897  infssuzcl  12898  supxrbnd  13289  supxrgtmnf  13290  supxrre1  13291  supxrre2  13292  supxrss  13293  infxrss  13300  iccsupr  13401  hashf1lem2  14399  trclun  14943  fsum2d  15699  fsumabs  15729  fsumrlim  15739  fsumo1  15740  fprod2d  15907  rpnnen2lem4  16142  rpnnen2lem7  16145  ramub2  16929  ressinbas  17172  ressress  17175  submre  17531  mrcss  17542  mreacs  17584  drsdirfi  18240  clatglbss  18454  ipopos  18471  cntz2ss  19163  pgrpsubgsymg  19241  ablfac1eulem  19901  subrgint  20335  tgval  22387  mretopd  22525  ssnei  22543  opnneiss  22551  restdis  22611  restcls  22614  restntr  22615  tgcnp  22686  fbssfi  23270  fgss2  23307  fgcl  23311  supfil  23328  alexsubALTlem3  23482  alexsubALTlem4  23483  cnextcn  23500  ustex3sym  23651  trust  23663  restutop  23671  utop2nei  23684  cfiluweak  23729  blssexps  23861  blssex  23862  mopni3  23932  metss  23946  metcnp3  23978  metust  23996  cfilucfil  23997  psmetutop  24005  tgioo  24241  xrsmopn  24257  fsumcn  24315  cncfmptid  24358  iscmet3lem2  24738  caussi  24743  ovolsslem  24930  ovolsscl  24932  ovolssnul  24933  opnmblALT  25049  itgfsum  25273  limcresi  25331  dvmptfsum  25421  plyss  25642  madebdayim  27305  cofcutrtime  27334  nbuhgr  28465  chsupunss  30460  shsupunss  30462  spanss  30464  shslubi  30501  shlub  30530  mdsl1i  31437  mdsl2i  31438  cvmdi  31440  mdslmd1lem1  31441  mdslmd1lem2  31442  mdslmd2i  31446  mdslmd4i  31449  atomli  31498  atcvatlem  31501  chirredlem2  31507  chirredi  31510  mdsymlem5  31523  xrge0infss  31844  tpr2rico  32723  sigainb  32965  dya2icoseg2  33108  omssubadd  33130  eulerpartlemn  33211  ballotlem2  33318  nummin  33925  cvmlift2lem12  34136  opnbnd  35014  fneint  35037  dissneqlem  36025  inunissunidif  36060  pibt2  36102  fin2so  36279  matunitlindflem1  36288  mblfinlem4  36332  ismblfin  36333  filbcmb  36413  heiborlem10  36493  igenmin  36737  lssatle  37690  paddss1  38493  paddss2  38494  paddss12  38495  paddssw2  38520  pclssN  38570  pclfinN  38576  polsubN  38583  2polvalN  38590  2polssN  38591  3polN  38592  2pmaplubN  38602  pnonsingN  38609  polsubclN  38628  dihord6apre  39932  dochsscl  40044  mapdordlem2  40313  isnacs3  41219  itgoss  41676  ofoaid1  41879  ofoaid2  41880  sspwimp  43450  sspwimpVD  43451  nsstr  43555  islptre  44108  gsumlsscl  46707  lincellss  46755  ellcoellss  46764