MPE Home Metamath Proof Explorer < Previous   Next >
Nearby theorems
Mirrors  >  Home  >  MPE Home  >  Th. List  >  sstr Structured version   Visualization version   GIF version

Theorem sstr 3806
Description: Transitivity of subclasses. Theorem 6 of [Suppes] p. 23. (Contributed by NM, 5-Sep-2003.)
Assertion
Ref Expression
sstr ((𝐴𝐵𝐵𝐶) → 𝐴𝐶)

Proof of Theorem sstr
StepHypRef Expression
1 sstr2 3805 . 2 (𝐴𝐵 → (𝐵𝐶𝐴𝐶))
21imp 395 1 ((𝐴𝐵𝐵𝐶) → 𝐴𝐶)
Colors of variables: wff setvar class
Syntax hints:  wi 4  wa 384  wss 3769
This theorem was proved from axioms:  ax-mp 5  ax-1 6  ax-2 7  ax-3 8  ax-gen 1877  ax-4 1894  ax-5 2001  ax-6 2068  ax-7 2104  ax-9 2165  ax-10 2185  ax-11 2201  ax-12 2214  ax-ext 2784
This theorem depends on definitions:  df-bi 198  df-an 385  df-or 866  df-tru 1641  df-ex 1860  df-nf 1864  df-sb 2061  df-clab 2793  df-cleq 2799  df-clel 2802  df-in 3776  df-ss 3783
This theorem is referenced by:  sstrd  3808  sylan9ss  3811  ssdifss  3940  uneqin  4080  ssrnres  5783  relrelss  5873  fco  6269  fssres  6281  ssimaex  6480  dff3  6590  tpostpos2  7604  smores  7681  om00  7888  omeulem2  7896  pmss12g  8115  unblem1  8447  unblem2  8448  unblem3  8449  unblem4  8450  isfinite2  8453  cantnfval2  8809  cantnfle  8811  rankxplim3  8987  alephinit  9197  dfac12lem2  9247  ackbij1lem11  9333  cfeq0  9359  cfsuc  9360  cff1  9361  cflim2  9366  cfss  9368  cfslb2n  9371  cofsmo  9372  cfsmolem  9373  fin23lem34  9449  fin1a2lem13  9515  axdc3lem2  9554  axdclem  9622  pwcfsdom  9686  wunfi  9824  tskxpss  9875  tskcard  9884  suprzcl  11719  uzwo  11966  uzwo2  11967  infssuzle  11986  infssuzcl  11987  supxrbnd  12372  supxrgtmnf  12373  supxrre1  12374  supxrre2  12375  supxrss  12376  infxrss  12383  iccsupr  12481  hashf1lem2  13453  trclun  13974  fsum2d  14721  fsumabs  14751  fsumrlim  14761  fsumo1  14762  fprod2d  14928  rpnnen2lem4  15162  rpnnen2lem7  15165  ramub2  15931  ressinbas  16143  ressress  16146  submre  16466  mrcss  16477  mreacs  16519  drsdirfi  17139  clatglbss  17328  ipopos  17361  cntz2ss  17962  ablfac1eulem  18669  subrgint  19002  tgval  20969  mretopd  21106  ssnei  21124  opnneiss  21132  restdis  21192  restcls  21195  restntr  21196  tgcnp  21267  fbssfi  21850  fgss2  21887  fgcl  21891  supfil  21908  alexsubALTlem3  22062  alexsubALTlem4  22063  cnextcn  22080  ustex3sym  22230  trust  22242  restutop  22250  utop2nei  22263  cfiluweak  22308  blssexps  22440  blssex  22441  mopni3  22508  metss  22522  metcnp3  22554  metust  22572  cfilucfil  22573  psmetutop  22581  tgioo  22808  xrsmopn  22824  fsumcn  22882  cncfmptid  22924  iscmet3lem2  23298  caussi  23303  ovolsslem  23461  ovolsscl  23463  ovolssnul  23464  opnmblALT  23580  itgfsum  23803  limcresi  23859  dvmptfsum  23948  plyss  24165  nbuhgr  26451  chsupunss  28527  shsupunss  28529  spanss  28531  shslubi  28568  shlub  28597  mdsl1i  29504  mdsl2i  29505  cvmdi  29507  mdslmd1lem1  29508  mdslmd1lem2  29509  mdslmd2i  29513  mdslmd4i  29516  atomli  29565  atcvatlem  29568  chirredlem2  29574  chirredi  29577  mdsymlem5  29590  xrge0infss  29848  tpr2rico  30279  sigainb  30520  dya2icoseg2  30661  omssubadd  30683  eulerpartlemn  30764  ballotlem2  30871  cvmlift2lem12  31614  opnbnd  32636  fneint  32659  bj-intss  33359  dissneqlem  33499  fin2so  33704  matunitlindflem1  33713  mblfinlem4  33757  ismblfin  33758  filbcmb  33842  heiborlem10  33925  igenmin  34169  lssatle  34790  paddss1  35592  paddss2  35593  paddss12  35594  paddssw2  35619  pclssN  35669  pclfinN  35675  polsubN  35682  2polvalN  35689  2polssN  35690  3polN  35691  2pmaplubN  35701  pnonsingN  35708  polsubclN  35727  dihord6apre  37031  dochsscl  37143  mapdordlem2  37412  isnacs3  37769  itgoss  38228  sspwimp  39642  sspwimpVD  39643  nsstr  39760  islptre  40325  gsumlsscl  42726  lincellss  42777  ellcoellss  42786
  Copyright terms: Public domain W3C validator