MPE Home Metamath Proof Explorer < Previous   Next >
Nearby theorems
Mirrors  >  Home  >  MPE Home  >  Th. List  >  sstri Unicode version

Theorem sstri 3188
Description: Subclass transitivity inference. (Contributed by NM, 5-May-2000.)
Hypotheses
Ref Expression
sstri.1  |-  A  C_  B
sstri.2  |-  B  C_  C
Assertion
Ref Expression
sstri  |-  A  C_  C

Proof of Theorem sstri
StepHypRef Expression
1 sstri.1 . 2  |-  A  C_  B
2 sstri.2 . 2  |-  B  C_  C
3 sstr2 3186 . 2  |-  ( A 
C_  B  ->  ( B  C_  C  ->  A  C_  C ) )
41, 2, 3mp2 17 1  |-  A  C_  C
Colors of variables: wff set class
Syntax hints:    C_ wss 3152
This theorem is referenced by:  snsstp1  3766  snsstp2  3767  uniintsn  3899  dmexg  4939  rnexg  4940  ssrnres  5116  cossxp  5195  fabexg  5422  foimacnv  5490  ssimaex  5584  oprabss  5933  fparlem3  6220  fparlem4  6221  tposssxp  6238  riotassuni  6343  mapsspw  6803  sbthlem5  6975  sbthlem7  6977  marypha1lem  7186  ordtypelem4  7236  hartogslem1  7257  tc2  7427  tz9.12lem1  7459  rankval4  7539  rankxpl  7547  rankxplim  7549  infxpenlem  7641  ackbij1lem18  7863  cflm  7876  fin23lem29  7967  hsmexlem4  8055  hsmexlem5  8056  brdom3  8153  brdom5  8154  brdom4  8155  smobeth  8208  pwfseqlem3  8282  wundm  8350  wunrn  8351  wunex2  8360  ltsopi  8512  dmaddpi  8514  dmmulpi  8515  nqerf  8554  ltrelxr  8886  nnsscn  9751  nn0sscn  9970  uzwo2  10283  uzinfmi  10297  infmssuzle  10300  infmssuzcl  10301  uzwo3  10311  nn0ssq  10324  nnssq  10325  qsscn  10327  rpnnen1lem3  10344  rpnnen1lem5  10346  dflt2  10482  fzval2  10785  fzof  10872  flval3  10945  uzsup  10967  uzrdgfni  11021  expcl2lem  11115  rpexpcl  11122  expge0  11138  expge1  11139  hashxrcl  11351  seqcoll  11401  wrdexg  11425  seqshft  11580  sqrlem3  11730  limsupval2  11954  limsupgre  11955  rlimpm  11974  rlimclim  12020  isercolllem1  12138  isercolllem2  12139  isercoll  12141  caurcvg  12149  caucvg  12151  summolem2a  12188  summolem2  12189  zsum  12191  fsumcvg3  12202  fsumrpcl  12210  fsumge0  12253  climfsum  12278  ackbijnn  12286  divalglem8  12599  sadaddlem  12657  isprm3  12767  maxprmfct  12792  pclem  12891  prmreclem1  12963  prmreclem2  12964  prmreclem3  12965  1arith  12974  4sqlem11  13002  ramtlecl  13047  ramcl2lem  13056  ramxrcl  13064  structfn  13161  strlemor1  13235  strleun  13238  srngbase  13264  srngplusg  13265  srngmulr  13266  lmodbase  13273  lmodplusg  13274  lmodsca  13275  algbase  13278  algaddg  13279  algmulr  13280  algsca  13281  algvsca  13282  phlbase  13288  phlplusg  13289  phlsca  13290  phlvsca  13291  phlip  13292  odrngbas  13312  odrngplusg  13313  odrngmulr  13314  odrngtset  13315  odrngle  13316  odrngds  13317  prdsval  13355  prdssca  13356  prdsbas  13357  prdsplusg  13358  prdsmulr  13359  prdsvsca  13360  prdsle  13361  prdsds  13363  prdstset  13365  prdshom  13366  prdsco  13367  imasbas  13415  imasds  13416  imasplusg  13420  imasmulr  13421  imassca  13422  imasvsca  13423  imastset  13424  imasle  13425  wunfunc  13773  fullfunc  13780  fthfunc  13781  isfull  13784  isfth  13788  wunnat  13830  dmcoass  13898  catcisolem  13938  catciso  13939  catcoppccl  13940  catcfuccl  13941  catcxpccl  13981  ipobas  14258  ipolerval  14259  ipotset  14260  psdmrn  14316  psss  14323  ledm  14346  lern  14347  dirdm  14356  dirge  14359  gexex  15145  gsumval3  15191  gsumzaddlem  15203  gsumconst  15209  gsumunsn  15221  lssacs  15724  asplss  16069  aspsubrg  16071  psrass1lem  16123  psrbas  16124  psrplusg  16126  psrmulr  16129  psrsca  16134  psrvscafval  16135  psrass1  16150  psrdi  16151  psrdir  16152  psrcom  16153  psrass23  16154  psropprmul  16316  coe1mul2  16346  cnfldbas  16383  cnfldadd  16384  cnfldmul  16385  cnfldcj  16386  cnfldtset  16387  cnfldle  16388  cnfldds  16389  zntoslem  16510  leordtval2  16942  lmbrf  16990  lmres  17028  fiuncmp  17131  1stckgenlem  17248  kgencn3  17253  ptbasfi  17276  xkoopn  17284  txcnmpt  17318  txkgen  17346  opnfbas  17537  fmfnfmlem4  17652  tsmsxplem1  17835  nmoffn  18220  nmofval  18223  nmogelb  18225  nmolb  18226  nmof  18228  qtopbas  18268  tgqioo  18306  re2ndc  18307  iitopon  18383  dfii3  18387  iimulcn  18436  xrhmeo  18444  cnheiborlem  18452  bndth  18456  lebnumii  18464  reparphti  18495  pcoass  18522  cphsqrcl  18620  lmmbrf  18688  iscauf  18706  caucfil  18709  lmclimf  18729  ovolfioo  18827  ovolficc  18828  ovolficcss  18829  ovolfsf  18831  ovollb  18838  ovolicc2lem3  18878  ovolicc2lem4  18879  ovolicc2  18881  volf  18888  volsup  18913  ovolfs2  18926  uniiccdif  18933  uniioovol  18934  uniiccvol  18935  uniioombllem2  18938  uniioombllem3a  18939  uniioombllem3  18940  uniioombllem4  18941  uniioombllem5  18942  uniioombl  18944  dyadmbllem  18954  dyadmbl  18955  opnmbllem  18956  opnmblALT  18958  volsup2  18960  vitalilem4  18966  vitalilem5  18967  vitali  18968  mbfimaopnlem  19010  mbflimsup  19021  i1f0  19042  i1f1  19045  itg11  19046  itg2mulc  19102  itg2gt0  19115  ellimc2  19227  limcresi  19235  dvreslem  19259  dvres2lem  19260  dvaddbr  19287  dvmulbr  19288  dvlipcn  19341  c1liplem1  19343  lhop1lem  19360  lhop1  19361  lhop2  19362  lhop  19363  dvfsumrlim  19378  ftc1cn  19390  itgsubstlem  19395  itgsubst  19396  mdegleb  19450  mdeglt  19451  mdegldg  19452  mdegxrcl  19453  mdegcl  19455  mdegaddle  19460  mdegmullem  19464  deg1mul3le  19502  ig1peu  19557  ig1pdvds  19562  aacjcl  19707  aannenlem2  19709  aannenlem3  19710  aalioulem2  19713  taylfval  19738  radcnvcl  19793  radcnvlt1  19794  radcnvle  19796  abelth  19817  abelth2  19818  pilem2  19828  pilem3  19829  pige3  19885  recosf1o  19897  resinf1o  19898  tanord1  19899  logcn  19994  dvlog  19998  dvlog2lem  19999  efopn  20005  logtayl  20007  cxpcn3  20088  loglesqr  20098  ssscongptld  20122  leibpi  20238  efrlim  20264  jensenlem1  20281  jensenlem2  20282  jensen  20283  amgm  20285  ftalem5  20314  efnnfsumcl  20340  efchtdvds  20397  dvdsmulf1o  20434  fsumdvdsmul  20435  lgsfcl2  20541  2sqlem6  20608  2sqlem8  20611  2sqlem9  20612  rpvmasumlem  20636  rpvmasum2  20661  dchrisum0re  20662  dchrisum0lem3  20668  dchrisum0  20669  rplogsum  20676  dirith2  20677  nmlno0lem  21371  hlimcaui  21816  chsspwh  21826  shsss  21892  chintcli  21910  shsleji  21949  shub1i  21953  shsval2i  21966  lejdii  22117  spanuni  22123  sshhococi  22125  spansnpji  22157  osumcori  22222  5oai  22240  3oalem6  22246  3oai  22247  pjssmii  22260  mayete3i  22307  mayete3iOLD  22308  mayetes3i  22309  nmlnop0iALT  22575  imaelshi  22638  pjnmopi  22728  pjclem1  22775  pjci  22780  mdslmd1lem1  22905  shatomistici  22941  hatomistici  22942  chpssati  22943  ballotlemfc0  23051  ballotlemfcc  23052  ballotlemiex  23060  ballotlemsup  23063  ballotlemsdom  23070  ballotlemsima  23074  ballotlemrv2  23080  ballotth  23096  xppreima  23211  fzossnn  23278  unitsscn  23280  xrsmulgzz  23307  xrge0iifhom  23319  fsumrp0cl  23334  iundisjfi  23363  iundisj2fi  23364  lmlimxrge0  23372  lmxrge0  23375  esumcst  23436  esumpfinvallem  23442  esumpfinval  23443  esumpfinvalf  23444  esumcvg  23454  imambfm  23567  elmbfmvol2  23572  subfacp1lem2a  23711  erdszelem4  23725  erdszelem5  23726  erdszelem7  23728  erdszelem8  23729  kur14lem7  23743  kur14lem9  23745  cvxpcon  23773  cvxscon  23774  rescon  23777  iccllyscon  23781  umgrass  23871  txpss3v  24418  txprel  24419  onint1  24888  dvreasin  24923  dvreacos  24924  areacirclem2  24925  areacirclem3  24926  areacirclem4  24927  relded  25740  relcat  25761  lemindclsbu  25995  finminlem  26231  comppfsc  26307  tailf  26324  filnetlem3  26329  caures  26476  reheibor  26563  diophin  26852  4rexfrabdioph  26879  6rexfrabdioph  26880  irrapxlem1  26907  irrapx1  26913  monotuz  27026  jm2.27dlem5  27106  uvcff  27240  hbtlem2  27328  mvdco  27388  f1omvdconj  27389  lhe4.4ex1a  27546  itgsin0pilem1  27744  itgsinexp  27749  wallispilem2  27815  relopabVD  28677  bnj1145  29023  bnj1286  29049  atlatmstc  29509  atlatle  29510  pmaple  29950  sspadd1  30004  sspadd2  30005
This theorem was proved from axioms:  ax-1 5  ax-2 6  ax-3 7  ax-mp 8  ax-gen 1533  ax-5 1544  ax-17 1603  ax-9 1635  ax-8 1643  ax-6 1703  ax-7 1708  ax-11 1715  ax-12 1866  ax-ext 2264
This theorem depends on definitions:  df-bi 177  df-an 360  df-tru 1310  df-ex 1529  df-nf 1532  df-sb 1630  df-clab 2270  df-cleq 2276  df-clel 2279  df-in 3159  df-ss 3166
  Copyright terms: Public domain W3C validator