Theorem sstr 3990

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

Syntax hints:   → wi 4   ∧ wa 397   ⊆ wss 3948

This theorem was proved from axioms:  ax-mp 5  ax-1 6  ax-2 7  ax-3 8  ax-gen 1798  ax-4 1812  ax-5 1914  ax-6 1972  ax-7 2012  ax-8 2109  ax-9 2117  ax-ext 2704

This theorem depends on definitions:  df-bi 206  df-an 398  df-tru 1545  df-ex 1783  df-sb 2069  df-clab 2711  df-cleq 2725  df-clel 2811  df-v 3477  df-in 3955  df-ss 3965

This theorem is referenced by:  sstrd  3992  sylan9ss  3995  ssdifss  4135  uneqin  4278  intss2  5111  ssrnres  6175  relrelss  6270  fcof  6738  fcoOLD  6740  fssres  6755  ssimaex  6974  dff3  7099  tpostpos2  8229  smores  8349  om00  8572  omeulem2  8580  cofonr  8670  naddunif  8689  pmss12g  8860  unblem1  9292  unblem2  9293  unblem3  9294  unblem4  9295  isfinite2  9298  cantnfval2  9661  cantnfle  9663  rankxplim3  9873  alephinit  10087  dfac12lem2  10136  ackbij1lem11  10222  cfeq0  10248  cfsuc  10249  cff1  10250  cflim2  10255  cfss  10257  cfslb2n  10260  cofsmo  10261  cfsmolem  10262  fin23lem34  10338  fin1a2lem13  10404  axdc3lem2  10443  axdclem  10511  pwcfsdom  10575  wunfi  10713  tskxpss  10764  tskcard  10773  suprzcl  12639  uzwo  12892  uzwo2  12893  infssuzle  12912  infssuzcl  12913  supxrbnd  13304  supxrgtmnf  13305  supxrre1  13306  supxrre2  13307  supxrss  13308  infxrss  13315  iccsupr  13416  hashf1lem2  14414  trclun  14958  fsum2d  15714  fsumabs  15744  fsumrlim  15754  fsumo1  15755  fprod2d  15922  rpnnen2lem4  16157  rpnnen2lem7  16160  ramub2  16944  ressinbas  17187  ressress  17190  submre  17546  mrcss  17557  mreacs  17599  drsdirfi  18255  clatglbss  18469  ipopos  18486  cntz2ss  19194  pgrpsubgsymg  19272  ablfac1eulem  19937  subrgint  20379  tgval  22450  mretopd  22588  ssnei  22606  opnneiss  22614  restdis  22674  restcls  22677  restntr  22678  tgcnp  22749  fbssfi  23333  fgss2  23370  fgcl  23374  supfil  23391  alexsubALTlem3  23545  alexsubALTlem4  23546  cnextcn  23563  ustex3sym  23714  trust  23726  restutop  23734  utop2nei  23747  cfiluweak  23792  blssexps  23924  blssex  23925  mopni3  23995  metss  24009  metcnp3  24041  metust  24059  cfilucfil  24060  psmetutop  24068  tgioo  24304  xrsmopn  24320  fsumcn  24378  cncfmptid  24421  iscmet3lem2  24801  caussi  24806  ovolsslem  24993  ovolsscl  24995  ovolssnul  24996  opnmblALT  25112  itgfsum  25336  limcresi  25394  dvmptfsum  25484  plyss  25705  madebdayim  27372  cofcutrtime  27404  nbuhgr  28590  chsupunss  30585  shsupunss  30587  spanss  30589  shslubi  30626  shlub  30655  mdsl1i  31562  mdsl2i  31563  cvmdi  31565  mdslmd1lem1  31566  mdslmd1lem2  31567  mdslmd2i  31571  mdslmd4i  31574  atomli  31623  atcvatlem  31626  chirredlem2  31632  chirredi  31635  mdsymlem5  31648  xrge0infss  31961  tpr2rico  32881  sigainb  33123  dya2icoseg2  33266  omssubadd  33288  eulerpartlemn  33369  ballotlem2  33476  nummin  34083  cvmlift2lem12  34294  opnbnd  35199  fneint  35222  dissneqlem  36210  inunissunidif  36245  pibt2  36287  fin2so  36464  matunitlindflem1  36473  mblfinlem4  36517  ismblfin  36518  filbcmb  36597  heiborlem10  36677  igenmin  36921  lssatle  37874  paddss1  38677  paddss2  38678  paddss12  38679  paddssw2  38704  pclssN  38754  pclfinN  38760  polsubN  38767  2polvalN  38774  2polssN  38775  3polN  38776  2pmaplubN  38786  pnonsingN  38793  polsubclN  38812  dihord6apre  40116  dochsscl  40228  mapdordlem2  40497  isnacs3  41434  itgoss  41891  ofoaid1  42094  ofoaid2  42095  sspwimp  43665  sspwimpVD  43666  nsstr  43770  islptre  44322  subrngint  46724  gsumlsscl  47013  lincellss  47061  ellcoellss  47070