Theorem sstr 3644

Description: Transitivity of subclasses. 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 3643	. 2 ⊢ (𝐴 ⊆ 𝐵 → (𝐵 ⊆ 𝐶 → 𝐴 ⊆ 𝐶))
2	1	imp 444	1 ⊢ ((𝐴 ⊆ 𝐵 ∧ 𝐵 ⊆ 𝐶) → 𝐴 ⊆ 𝐶)

Syntax hints:   → wi 4   ∧ wa 383   ⊆ wss 3607

This theorem was proved from axioms:  ax-mp 5  ax-1 6  ax-2 7  ax-3 8  ax-gen 1762  ax-4 1777  ax-5 1879  ax-6 1945  ax-7 1981  ax-9 2039  ax-10 2059  ax-11 2074  ax-12 2087  ax-13 2282  ax-ext 2631

This theorem depends on definitions:  df-bi 197  df-or 384  df-an 385  df-tru 1526  df-ex 1745  df-nf 1750  df-sb 1938  df-clab 2638  df-cleq 2644  df-clel 2647  df-in 3614  df-ss 3621

This theorem is referenced by:  sstrd  3646  sylan9ss  3649  ssdifss  3774  uneqin  3911  ssrnres  5607  relrelss  5697  fco  6096  fssres  6108  ssimaex  6302  dff3  6412  tpostpos2  7418  smores  7494  om00  7700  omeulem2  7708  pmss12g  7926  unblem1  8253  unblem2  8254  unblem3  8255  unblem4  8256  isfinite2  8259  cantnfval2  8604  cantnfle  8606  rankxplim3  8782  alephinit  8956  dfac12lem2  9004  ackbij1lem11  9090  cfeq0  9116  cfsuc  9117  cff1  9118  cflim2  9123  cfss  9125  cfslb2n  9128  cofsmo  9129  cfsmolem  9130  fin23lem34  9206  fin1a2lem13  9272  axdc3lem2  9311  axdclem  9379  pwcfsdom  9443  wunfi  9581  tskxpss  9632  tskcard  9641  suprzcl  11495  uzwo  11789  uzwo2  11790  infssuzle  11809  infssuzcl  11810  supxrbnd  12196  supxrgtmnf  12197  supxrre1  12198  supxrre2  12199  supxrss  12200  infxrss  12207  iccsupr  12304  hashf1lem2  13278  trclun  13799  fsum2d  14546  fsumabs  14577  fsumrlim  14587  fsumo1  14588  fprod2d  14755  rpnnen2lem4  14990  rpnnen2lem7  14993  ramub2  15765  ressinbas  15983  ressress  15985  submre  16312  mrcss  16323  mreacs  16366  drsdirfi  16985  clatglbss  17174  ipopos  17207  cntz2ss  17811  ablfac1eulem  18517  subrgint  18850  tgval  20807  mretopd  20944  ssnei  20962  opnneiss  20970  restdis  21030  restcls  21033  restntr  21034  tgcnp  21105  fbssfi  21688  fgss2  21725  fgcl  21729  supfil  21746  alexsubALTlem3  21900  alexsubALTlem4  21901  cnextcn  21918  ustex3sym  22068  trust  22080  restutop  22088  utop2nei  22101  cfiluweak  22146  blssexps  22278  blssex  22279  mopni3  22346  metss  22360  metcnp3  22392  metust  22410  cfilucfil  22411  psmetutop  22419  tgioo  22646  xrsmopn  22662  fsumcn  22720  cncfmptid  22762  iscmet3lem2  23136  caussi  23141  ovolsslem  23298  ovolsscl  23300  ovolssnul  23301  opnmblALT  23417  itgfsum  23638  limcresi  23694  dvmptfsum  23783  plyss  24000  nbuhgr  26284  chsupunss  28331  shsupunss  28333  spanss  28335  shslubi  28372  shlub  28401  mdsl1i  29308  mdsl2i  29309  cvmdi  29311  mdslmd1lem1  29312  mdslmd1lem2  29313  mdslmd2i  29317  mdslmd4i  29320  atomli  29369  atcvatlem  29372  chirredlem2  29378  chirredi  29381  mdsymlem5  29394  xrge0infss  29653  tpr2rico  30086  sigainb  30327  dya2icoseg2  30468  omssubadd  30490  eulerpartlemn  30571  ballotlem2  30678  cvmlift2lem12  31422  opnbnd  32445  fneint  32468  bj-intss  33178  dissneqlem  33317  fin2so  33526  matunitlindflem1  33535  mblfinlem4  33579  ismblfin  33580  filbcmb  33665  heiborlem10  33749  igenmin  33993  lssatle  34620  paddss1  35421  paddss2  35422  paddss12  35423  paddssw2  35448  pclssN  35498  pclfinN  35504  polsubN  35511  2polvalN  35518  2polssN  35519  3polN  35520  2pmaplubN  35530  pnonsingN  35537  polsubclN  35556  dihord6apre  36862  dochsscl  36974  mapdordlem2  37243  isnacs3  37590  itgoss  38050  sspwimp  39468  sspwimpVD  39469  nsstr  39587  islptre  40169  gsumlsscl  42489  lincellss  42540  ellcoellss  42549