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

Theorem sstri 3325
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 3323 . 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 3288
This theorem is referenced by:  snsstp1  3917  snsstp2  3918  uniintsn  4055  dmexg  5097  rnexg  5098  ssrnres  5276  cossxp  5359  fabexg  5591  foimacnv  5659  ssimaex  5755  oprabss  6126  fparlem3  6415  fparlem4  6416  tposssxp  6450  riotassuni  6555  mapsspw  7016  sbthlem5  7188  sbthlem7  7190  marypha1lem  7404  ordtypelem4  7454  hartogslem1  7475  tc2  7645  tz9.12lem1  7677  rankval4  7757  rankxpl  7765  rankxplim  7767  infxpenlem  7859  ackbij1lem18  8081  cflm  8094  fin23lem29  8185  hsmexlem4  8273  hsmexlem5  8274  brdom3  8370  brdom5  8371  brdom4  8372  smobeth  8425  pwfseqlem3  8499  wundm  8567  wunrn  8568  wunex2  8577  ltsopi  8729  dmaddpi  8731  dmmulpi  8732  nqerf  8771  ltrelxr  9103  nnsscn  9969  nn0sscn  10190  uzwo2  10505  uzinfmi  10519  infmssuzle  10522  infmssuzcl  10523  uzwo3  10533  nn0ssq  10546  nnssq  10547  qsscn  10549  rpnnen1lem3  10566  rpnnen1lem5  10568  dflt2  10705  fzval2  11010  fzof  11100  fzossnn  11135  injresinj  11163  flval3  11185  uzsup  11207  uzrdgfni  11261  expcl2lem  11356  rpexpcl  11363  expge0  11379  expge1  11380  hashxrcl  11603  seqcoll  11675  wrdexg  11702  seqshft  11863  sqrlem3  12013  limsupval2  12237  limsupgre  12238  rlimpm  12257  rlimclim  12303  isercolllem1  12421  isercolllem2  12422  isercoll  12424  caurcvg  12433  caucvg  12435  summolem2a  12472  summolem2  12473  zsum  12475  fsumcvg3  12486  fsumrpcl  12494  fsumge0  12537  climfsum  12562  ackbijnn  12570  divalglem8  12883  sadaddlem  12941  isprm3  13051  maxprmfct  13076  pclem  13175  prmreclem1  13247  prmreclem2  13248  prmreclem3  13249  1arith  13258  4sqlem11  13286  ramtlecl  13331  ramcl2lem  13340  ramxrcl  13348  structfn  13445  strlemor1  13519  strleun  13522  srngbase  13548  srngplusg  13549  srngmulr  13550  lmodbase  13557  lmodplusg  13558  lmodsca  13559  algbase  13562  algaddg  13563  algmulr  13564  algsca  13565  algvsca  13566  phlbase  13572  phlplusg  13573  phlsca  13574  phlvsca  13575  phlip  13576  odrngbas  13598  odrngplusg  13599  odrngmulr  13600  odrngtset  13601  odrngle  13602  odrngds  13603  prdsval  13641  prdssca  13642  prdsbas  13643  prdsplusg  13644  prdsmulr  13645  prdsvsca  13646  prdsle  13647  prdsds  13649  prdstset  13651  prdshom  13652  prdsco  13653  imasbas  13701  imasds  13702  imasplusg  13706  imasmulr  13707  imassca  13708  imasvsca  13709  imastset  13710  imasle  13711  wunfunc  14059  fullfunc  14066  fthfunc  14067  isfull  14070  isfth  14074  wunnat  14116  dmcoass  14184  catcisolem  14224  catciso  14225  catcoppccl  14226  catcfuccl  14227  catcxpccl  14267  ipobas  14544  ipolerval  14545  ipotset  14546  psdmrn  14602  psss  14609  ledm  14632  lern  14633  dirdm  14642  dirge  14645  gexex  15431  gsumval3  15477  gsumzaddlem  15489  gsumconst  15495  gsumunsn  15507  lssacs  16006  asplss  16351  aspsubrg  16353  psrass1lem  16405  psrbas  16406  psrplusg  16408  psrmulr  16411  psrsca  16416  psrvscafval  16417  psrass1  16432  psrdi  16433  psrdir  16434  psrcom  16435  psrass23  16436  psropprmul  16595  coe1mul2  16625  cnfldbas  16670  cnfldadd  16671  cnfldmul  16672  cnfldcj  16673  cnfldtset  16674  cnfldle  16675  cnfldds  16676  cnfldunif  16677  zntoslem  16800  leordtval2  17238  lmbrf  17286  lmres  17326  fiuncmp  17429  1stckgenlem  17546  kgencn3  17551  ptbasfi  17574  xkoopn  17582  txcnmpt  17617  txkgen  17645  opnfbas  17835  fmfnfmlem4  17950  tsmsxplem1  18143  trust  18220  restutop  18228  nmoffn  18706  nmofval  18709  nmogelb  18711  nmolb  18712  nmof  18714  qtopbas  18754  tgqioo  18792  re2ndc  18793  iitopon  18870  dfii3  18874  iimulcn  18924  cnheiborlem  18940  bndth  18944  lebnumii  18952  reparphti  18983  pcoass  19010  cphsqrcl  19108  lmmbrf  19176  iscauf  19194  caucfil  19197  lmclimf  19217  ovolfioo  19325  ovolficc  19326  ovolficcss  19327  ovolfsf  19329  ovollb  19336  ovolicc2lem3  19376  ovolicc2lem4  19377  ovolicc2  19379  volf  19386  volsup  19411  ovolfs2  19424  uniiccdif  19431  uniioovol  19432  uniiccvol  19433  uniioombllem2  19436  uniioombllem3a  19437  uniioombllem3  19438  uniioombllem4  19439  uniioombllem5  19440  uniioombl  19442  dyadmbllem  19452  dyadmbl  19453  opnmbllem  19454  opnmblALT  19456  volsup2  19458  vitalilem4  19464  vitalilem5  19465  vitali  19466  mbfimaopnlem  19508  mbflimsup  19519  i1f0  19540  i1f1  19543  itg11  19544  itg2mulc  19600  itg2gt0  19613  ellimc2  19725  limcresi  19733  dvreslem  19757  dvres2lem  19758  dvaddbr  19785  dvmulbr  19786  dvlipcn  19839  c1liplem1  19841  lhop1lem  19858  lhop1  19859  lhop2  19860  lhop  19861  dvfsumrlim  19876  ftc1cn  19888  itgsubstlem  19893  itgsubst  19894  mdegleb  19948  mdeglt  19949  mdegldg  19950  mdegxrcl  19951  mdegcl  19953  mdegaddle  19958  mdegmullem  19962  deg1mul3le  20000  ig1peu  20055  ig1pdvds  20060  aacjcl  20205  aannenlem2  20207  aannenlem3  20208  aalioulem2  20211  taylfval  20236  radcnvcl  20294  radcnvlt1  20295  radcnvle  20297  abelth  20318  abelth2  20319  pilem2  20329  pilem3  20330  pige3  20386  recosf1o  20398  resinf1o  20399  tanord1  20400  logcn  20499  dvlog  20503  dvlog2lem  20504  efopn  20510  logtayl  20512  cxpcn3  20593  loglesqr  20603  ssscongptld  20627  leibpi  20743  efrlim  20769  jensenlem1  20786  jensenlem2  20787  jensen  20788  amgm  20790  ftalem5  20820  efnnfsumcl  20846  efchtdvds  20903  dvdsmulf1o  20940  fsumdvdsmul  20941  lgsfcl2  21047  2sqlem6  21114  2sqlem8  21117  2sqlem9  21118  rpvmasumlem  21142  rpvmasum2  21167  dchrisum0re  21168  dchrisum0lem3  21174  dchrisum0  21175  rplogsum  21182  dirith2  21183  umgrass  21315  constr3pthlem1  21603  nmlno0lem  22255  hlimcaui  22700  chsspwh  22710  shsss  22776  chintcli  22794  shsleji  22833  shub1i  22837  shsval2i  22850  lejdii  23001  spanuni  23007  sshhococi  23009  spansnpji  23041  osumcori  23106  5oai  23124  3oalem6  23130  3oai  23131  pjssmii  23144  mayete3i  23191  mayete3iOLD  23192  mayetes3i  23193  nmlnop0iALT  23459  imaelshi  23522  pjnmopi  23612  pjclem1  23659  pjci  23664  mdslmd1lem1  23789  shatomistici  23825  hatomistici  23826  chpssati  23827  xppreima  24020  iundisjfi  24113  iundisj2fi  24114  xrsmulgzz  24161  fsumrp0cl  24178  unitsscn  24255  xrge0iifhom  24284  lmlimxrge0  24295  lmxrge0  24298  esumcst  24416  esumpfinvallem  24425  esumpfinval  24426  esumpfinvalf  24427  esumcvg  24437  measunl  24531  imambfm  24573  elmbfmvol2  24578  sxbrsigalem3  24583  sxbrsigalem2  24597  sxbrsigalem4  24598  sitgclg  24617  ballotlemfc0  24711  ballotlemfcc  24712  ballotlemiex  24720  ballotlemsup  24723  ballotlemsdom  24730  ballotlemsima  24734  ballotlemrv2  24740  ballotth  24756  lgamgulmlem2  24775  subfacp1lem2a  24827  erdszelem4  24841  erdszelem5  24842  erdszelem7  24844  erdszelem8  24845  kur14lem7  24859  kur14lem9  24861  cvxpcon  24890  cvxscon  24891  rescon  24894  iccllyscon  24898  prodmolem2a  25221  prodmolem2  25222  zprod  25224  fprodrpcl  25243  rprisefaccl  25299  txpss3v  25640  txprel  25641  onint1  26111  mblfinlem  26151  mblfinlem2  26152  mblfinlem3  26153  ismblfin  26154  mbfposadd  26161  cnambfre  26162  itg2addnc  26166  ftc1cnnclem  26185  ftc1cnnc  26186  dvreasin  26187  dvreacos  26188  areacirclem2  26189  areacirclem3  26190  areacirclem4  26191  finminlem  26219  comppfsc  26285  tailf  26302  filnetlem3  26307  caures  26364  reheibor  26446  diophin  26729  4rexfrabdioph  26756  6rexfrabdioph  26757  irrapxlem1  26783  irrapx1  26789  monotuz  26902  jm2.27dlem5  26982  uvcff  27116  hbtlem2  27204  mvdco  27264  f1omvdconj  27265  lhe4.4ex1a  27422  itgsin0pilem1  27619  itgsinexplem1  27623  itgsinexp  27624  wallispilem2  27690  relopabVD  28731  bnj1145  29080  bnj1286  29106  atlatmstc  29814  atlatle  29815  pmaple  30255  sspadd1  30309  sspadd2  30310
This theorem was proved from axioms:  ax-1 5  ax-2 6  ax-3 7  ax-mp 8  ax-gen 1552  ax-5 1563  ax-17 1623  ax-9 1662  ax-8 1683  ax-6 1740  ax-7 1745  ax-11 1757  ax-12 1946  ax-ext 2393
This theorem depends on definitions:  df-bi 178  df-an 361  df-tru 1325  df-ex 1548  df-nf 1551  df-sb 1656  df-clab 2399  df-cleq 2405  df-clel 2408  df-in 3295  df-ss 3302
  Copyright terms: Public domain W3C validator