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

Theorem sstri 3358
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 3356 . 2  |-  ( A 
C_  B  ->  ( B  C_  C  ->  A  C_  C ) )
41, 2, 3mp2 9 1  |-  A  C_  C
Colors of variables: wff set class
Syntax hints:    C_ wss 3321
This theorem is referenced by:  snsstp1  3950  snsstp2  3951  uniintsn  4088  dmexg  5131  rnexg  5132  ssrnres  5310  cossxp  5393  fabexg  5625  foimacnv  5693  ssimaex  5789  oprabss  6160  fparlem3  6449  fparlem4  6450  tposssxp  6484  riotassuni  6589  mapsspw  7050  sbthlem5  7222  sbthlem7  7224  marypha1lem  7439  ordtypelem4  7491  hartogslem1  7512  tc2  7682  tz9.12lem1  7714  rankval4  7794  rankxpl  7802  rankxplim  7804  infxpenlem  7896  ackbij1lem18  8118  cflm  8131  fin23lem29  8222  hsmexlem4  8310  hsmexlem5  8311  brdom3  8407  brdom5  8408  brdom4  8409  smobeth  8462  pwfseqlem3  8536  wundm  8604  wunrn  8605  wunex2  8614  ltsopi  8766  dmaddpi  8768  dmmulpi  8769  nqerf  8808  ltrelxr  9140  nnsscn  10006  nn0sscn  10227  uzwo2  10542  uzinfmi  10556  infmssuzle  10559  infmssuzcl  10560  uzwo3  10570  nn0ssq  10583  nnssq  10584  qsscn  10586  rpnnen1lem3  10603  rpnnen1lem5  10605  dflt2  10742  fzval2  11047  fzof  11138  fzossnn  11173  injresinj  11201  flval3  11223  uzsup  11245  uzrdgfni  11299  expcl2lem  11394  rpexpcl  11401  expge0  11417  expge1  11418  hashxrcl  11641  seqcoll  11713  wrdexg  11740  seqshft  11901  sqrlem3  12051  limsupval2  12275  limsupgre  12276  rlimpm  12295  rlimclim  12341  isercolllem1  12459  isercolllem2  12460  isercoll  12462  caurcvg  12471  caucvg  12473  summolem2a  12510  summolem2  12511  zsum  12513  fsumcvg3  12524  fsumrpcl  12532  fsumge0  12575  climfsum  12600  ackbijnn  12608  divalglem8  12921  sadaddlem  12979  isprm3  13089  maxprmfct  13114  pclem  13213  prmreclem1  13285  prmreclem2  13286  prmreclem3  13287  1arith  13296  4sqlem11  13324  ramtlecl  13369  ramcl2lem  13378  ramxrcl  13386  structfn  13483  strlemor1  13557  strleun  13560  srngbase  13586  srngplusg  13587  srngmulr  13588  lmodbase  13595  lmodplusg  13596  lmodsca  13597  algbase  13600  algaddg  13601  algmulr  13602  algsca  13603  algvsca  13604  phlbase  13610  phlplusg  13611  phlsca  13612  phlvsca  13613  phlip  13614  odrngbas  13636  odrngplusg  13637  odrngmulr  13638  odrngtset  13639  odrngle  13640  odrngds  13641  prdsval  13679  prdssca  13680  prdsbas  13681  prdsplusg  13682  prdsmulr  13683  prdsvsca  13684  prdsle  13685  prdsds  13687  prdstset  13689  prdshom  13690  prdsco  13691  imasbas  13739  imasds  13740  imasplusg  13744  imasmulr  13745  imassca  13746  imasvsca  13747  imastset  13748  imasle  13749  wunfunc  14097  fullfunc  14104  fthfunc  14105  isfull  14108  isfth  14112  wunnat  14154  dmcoass  14222  catcisolem  14262  catciso  14263  catcoppccl  14264  catcfuccl  14265  catcxpccl  14305  ipobas  14582  ipolerval  14583  ipotset  14584  psdmrn  14640  psss  14647  ledm  14670  lern  14671  dirdm  14680  dirge  14683  gexex  15469  gsumval3  15515  gsumzaddlem  15527  gsumconst  15533  gsumunsn  15545  lssacs  16044  asplss  16389  aspsubrg  16391  psrass1lem  16443  psrbas  16444  psrplusg  16446  psrmulr  16449  psrsca  16454  psrvscafval  16455  psrass1  16470  psrdi  16471  psrdir  16472  psrcom  16473  psrass23  16474  psropprmul  16633  coe1mul2  16663  cnfldbas  16708  cnfldadd  16709  cnfldmul  16710  cnfldcj  16711  cnfldtset  16712  cnfldle  16713  cnfldds  16714  cnfldunif  16715  zntoslem  16838  leordtval2  17277  lmbrf  17325  lmres  17365  fiuncmp  17468  1stckgenlem  17586  kgencn3  17591  ptbasfi  17614  xkoopn  17622  txcnmpt  17657  txkgen  17685  opnfbas  17875  fmfnfmlem4  17990  tsmsxplem1  18183  trust  18260  restutop  18268  nmoffn  18746  nmofval  18749  nmogelb  18751  nmolb  18752  nmof  18754  qtopbas  18794  tgqioo  18832  re2ndc  18833  iitopon  18910  dfii3  18914  iimulcn  18964  cnheiborlem  18980  bndth  18984  lebnumii  18992  reparphti  19023  pcoass  19050  cphsqrcl  19148  lmmbrf  19216  iscauf  19234  caucfil  19237  lmclimf  19257  ovolfioo  19365  ovolficc  19366  ovolficcss  19367  ovolfsf  19369  ovollb  19376  ovolicc2lem3  19416  ovolicc2lem4  19417  ovolicc2  19419  volf  19426  volsup  19451  ovolfs2  19464  uniiccdif  19471  uniioovol  19472  uniiccvol  19473  uniioombllem2  19476  uniioombllem3a  19477  uniioombllem3  19478  uniioombllem4  19479  uniioombllem5  19480  uniioombl  19482  dyadmbllem  19492  dyadmbl  19493  opnmbllem  19494  opnmblALT  19496  volsup2  19498  vitalilem4  19504  vitalilem5  19505  vitali  19506  mbfimaopnlem  19548  mbflimsup  19559  i1f0  19580  i1f1  19583  itg11  19584  itg2mulc  19640  itg2gt0  19653  ellimc2  19765  limcresi  19773  dvreslem  19797  dvres2lem  19798  dvaddbr  19825  dvmulbr  19826  dvlipcn  19879  c1liplem1  19881  lhop1lem  19898  lhop1  19899  lhop2  19900  lhop  19901  dvfsumrlim  19916  ftc1cn  19928  itgsubstlem  19933  itgsubst  19934  mdegleb  19988  mdeglt  19989  mdegldg  19990  mdegxrcl  19991  mdegcl  19993  mdegaddle  19998  mdegmullem  20002  deg1mul3le  20040  ig1peu  20095  ig1pdvds  20100  aacjcl  20245  aannenlem2  20247  aannenlem3  20248  aalioulem2  20251  taylfval  20276  radcnvcl  20334  radcnvlt1  20335  radcnvle  20337  abelth  20358  abelth2  20359  pilem2  20369  pilem3  20370  pige3  20426  recosf1o  20438  resinf1o  20439  tanord1  20440  logcn  20539  dvlog  20543  dvlog2lem  20544  efopn  20550  logtayl  20552  cxpcn3  20633  loglesqr  20643  ssscongptld  20667  leibpi  20783  efrlim  20809  jensenlem1  20826  jensenlem2  20827  jensen  20828  amgm  20830  ftalem5  20860  efnnfsumcl  20886  efchtdvds  20943  dvdsmulf1o  20980  fsumdvdsmul  20981  lgsfcl2  21087  2sqlem6  21154  2sqlem8  21157  2sqlem9  21158  rpvmasumlem  21182  rpvmasum2  21207  dchrisum0re  21208  dchrisum0lem3  21214  dchrisum0  21215  rplogsum  21222  dirith2  21223  umgrass  21355  constr3pthlem1  21643  nmlno0lem  22295  hlimcaui  22740  chsspwh  22750  shsss  22816  chintcli  22834  shsleji  22873  shub1i  22877  shsval2i  22890  lejdii  23041  spanuni  23047  sshhococi  23049  spansnpji  23081  osumcori  23146  5oai  23164  3oalem6  23170  3oai  23171  pjssmii  23184  mayete3i  23231  mayete3iOLD  23232  mayetes3i  23233  nmlnop0iALT  23499  imaelshi  23562  pjnmopi  23652  pjclem1  23699  pjci  23704  mdslmd1lem1  23829  shatomistici  23865  hatomistici  23866  chpssati  23867  xppreima  24060  iundisjfi  24153  iundisj2fi  24154  xrsmulgzz  24201  fsumrp0cl  24218  unitsscn  24295  xrge0iifhom  24324  lmlimxrge0  24335  lmxrge0  24338  esumcst  24456  esumpfinvallem  24465  esumpfinval  24466  esumpfinvalf  24467  esumcvg  24477  measunl  24571  imambfm  24613  elmbfmvol2  24618  sxbrsigalem3  24623  sxbrsigalem2  24637  sxbrsigalem4  24638  sitgclg  24657  ballotlemfc0  24751  ballotlemfcc  24752  ballotlemiex  24760  ballotlemsup  24763  ballotlemsdom  24770  ballotlemsima  24774  ballotlemrv2  24780  ballotth  24796  lgamgulmlem2  24815  subfacp1lem2a  24867  erdszelem4  24881  erdszelem5  24882  erdszelem7  24884  erdszelem8  24885  kur14lem7  24899  kur14lem9  24901  cvxpcon  24930  cvxscon  24931  rescon  24934  iccllyscon  24938  prodmolem2a  25261  prodmolem2  25262  zprod  25264  fprodrpcl  25283  rprisefaccl  25340  txpss3v  25724  txprel  25725  limitssson  25757  onint1  26200  opnmbllem0  26243  mblfinlem1  26244  mblfinlem2  26245  mblfinlem3  26246  mblfinlem4  26247  ismblfin  26248  mbfposadd  26255  cnambfre  26256  itg2addnc  26260  ftc1cnnclem  26279  ftc1cnnc  26280  ftc1anclem3  26283  ftc1anclem7  26287  ftc1anc  26289  ftc2nc  26290  dvreasin  26291  dvreacos  26292  areacirclem1  26293  areacirclem2  26294  areacirc  26298  finminlem  26322  comppfsc  26388  tailf  26405  filnetlem3  26410  caures  26467  reheibor  26549  diophin  26832  4rexfrabdioph  26859  6rexfrabdioph  26860  irrapxlem1  26886  irrapx1  26892  monotuz  27005  jm2.27dlem5  27085  uvcff  27218  hbtlem2  27306  mvdco  27366  f1omvdconj  27367  lhe4.4ex1a  27524  itgsin0pilem1  27721  itgsinexplem1  27725  itgsinexp  27726  wallispilem2  27792  cshwssizelem3  28283  relopabVD  29014  bnj1145  29363  bnj1286  29389  atlatmstc  30118  atlatle  30119  pmaple  30559  sspadd1  30613  sspadd2  30614
This theorem was proved from axioms:  ax-1 5  ax-2 6  ax-3 7  ax-mp 8  ax-gen 1556  ax-5 1567  ax-17 1627  ax-9 1667  ax-8 1688  ax-6 1745  ax-7 1750  ax-11 1762  ax-12 1951  ax-ext 2418
This theorem depends on definitions:  df-bi 179  df-an 362  df-tru 1329  df-ex 1552  df-nf 1555  df-sb 1660  df-clab 2424  df-cleq 2430  df-clel 2433  df-in 3328  df-ss 3335
  Copyright terms: Public domain W3C validator