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

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

This theorem was proved from axioms:  ax-mp 5  ax-1 6  ax-2 7  ax-3 8  ax-gen 1790  ax-4 1804  ax-5 1906  ax-6 1964  ax-7 2004  ax-8 2101  ax-9 2109  ax-ext 2698

This theorem depends on definitions:  df-bi 206  df-an 396  df-tru 1537  df-ex 1775  df-sb 2061  df-clab 2705  df-cleq 2719  df-clel 2805  df-v 3471  df-in 3951  df-ss 3961

This theorem is referenced by:  sstrd  3988  sylan9ss  3991  ssdifss  4131  uneqin  4274  intss2  5105  ssrnres  6176  relrelss  6271  fcof  6740  fcoOLD  6742  fssres  6757  ssimaex  6977  dff3  7104  tpostpos2  8246  smores  8366  om00  8589  omeulem2  8597  cofonr  8688  naddunif  8707  pmss12g  8879  unblem1  9311  unblem2  9312  unblem3  9313  unblem4  9314  isfinite2  9317  cantnfval2  9684  cantnfle  9686  rankxplim3  9896  alephinit  10110  dfac12lem2  10159  ackbij1lem11  10245  cfeq0  10271  cfsuc  10272  cff1  10273  cflim2  10278  cfss  10280  cfslb2n  10283  cofsmo  10284  cfsmolem  10285  fin23lem34  10361  fin1a2lem13  10427  axdc3lem2  10466  axdclem  10534  pwcfsdom  10598  wunfi  10736  tskxpss  10787  tskcard  10796  suprzcl  12664  uzwo  12917  uzwo2  12918  infssuzle  12937  infssuzcl  12938  supxrbnd  13331  supxrgtmnf  13332  supxrre1  13333  supxrre2  13334  supxrss  13335  infxrss  13342  iccsupr  13443  hashf1lem2  14441  trclun  14985  fsum2d  15741  fsumabs  15771  fsumrlim  15781  fsumo1  15782  fprod2d  15949  rpnnen2lem4  16185  rpnnen2lem7  16188  ramub2  16974  ressinbas  17217  ressress  17220  submre  17576  mrcss  17587  mreacs  17629  drsdirfi  18288  clatglbss  18502  ipopos  18519  cntz2ss  19277  pgrpsubgsymg  19355  ablfac1eulem  20020  subrngint  20486  subrgint  20523  tgval  22845  mretopd  22983  ssnei  23001  opnneiss  23009  restdis  23069  restcls  23072  restntr  23073  tgcnp  23144  fbssfi  23728  fgss2  23765  fgcl  23769  supfil  23786  alexsubALTlem3  23940  alexsubALTlem4  23941  cnextcn  23958  ustex3sym  24109  trust  24121  restutop  24129  utop2nei  24142  cfiluweak  24187  blssexps  24319  blssex  24320  mopni3  24390  metss  24404  metcnp3  24436  metust  24454  cfilucfil  24455  psmetutop  24463  tgioo  24699  xrsmopn  24715  fsumcn  24775  cncfmptid  24820  iscmet3lem2  25207  caussi  25212  ovolsslem  25400  ovolsscl  25402  ovolssnul  25403  opnmblALT  25519  itgfsum  25743  limcresi  25801  dvmptfsum  25894  plyss  26120  madebdayim  27801  cofcutrtime  27834  nbuhgr  29143  chsupunss  31141  shsupunss  31143  spanss  31145  shslubi  31182  shlub  31211  mdsl1i  32118  mdsl2i  32119  cvmdi  32121  mdslmd1lem1  32122  mdslmd1lem2  32123  mdslmd2i  32127  mdslmd4i  32130  atomli  32179  atcvatlem  32182  chirredlem2  32188  chirredi  32191  mdsymlem5  32204  xrge0infss  32514  tpr2rico  33449  sigainb  33691  dya2icoseg2  33834  omssubadd  33856  eulerpartlemn  33937  ballotlem2  34044  nummin  34650  cvmlift2lem12  34860  opnbnd  35745  fneint  35768  dissneqlem  36755  inunissunidif  36790  pibt2  36832  fin2so  37015  matunitlindflem1  37024  mblfinlem4  37068  ismblfin  37069  filbcmb  37148  heiborlem10  37228  igenmin  37472  lssatle  38424  paddss1  39227  paddss2  39228  paddss12  39229  paddssw2  39254  pclssN  39304  pclfinN  39310  polsubN  39317  2polvalN  39324  2polssN  39325  3polN  39326  2pmaplubN  39336  pnonsingN  39343  polsubclN  39362  dihord6apre  40666  dochsscl  40778  mapdordlem2  41047  isnacs3  42052  itgoss  42509  ofoaid1  42710  ofoaid2  42711  sspwimp  44280  sspwimpVD  44281  nsstr  44384  islptre  44930  gsumlsscl  47370  lincellss  47417  ellcoellss  47426