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

Theorem sstri 3201
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 3199 . 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 3165
This theorem is referenced by:  snsstp1  3782  snsstp2  3783  uniintsn  3915  dmexg  4955  rnexg  4956  ssrnres  5132  cossxp  5211  fabexg  5438  foimacnv  5506  ssimaex  5600  oprabss  5949  fparlem3  6236  fparlem4  6237  tposssxp  6254  riotassuni  6359  mapsspw  6819  sbthlem5  6991  sbthlem7  6993  marypha1lem  7202  ordtypelem4  7252  hartogslem1  7273  tc2  7443  tz9.12lem1  7475  rankval4  7555  rankxpl  7563  rankxplim  7565  infxpenlem  7657  ackbij1lem18  7879  cflm  7892  fin23lem29  7983  hsmexlem4  8071  hsmexlem5  8072  brdom3  8169  brdom5  8170  brdom4  8171  smobeth  8224  pwfseqlem3  8298  wundm  8366  wunrn  8367  wunex2  8376  ltsopi  8528  dmaddpi  8530  dmmulpi  8531  nqerf  8570  ltrelxr  8902  nnsscn  9767  nn0sscn  9986  uzwo2  10299  uzinfmi  10313  infmssuzle  10316  infmssuzcl  10317  uzwo3  10327  nn0ssq  10340  nnssq  10341  qsscn  10343  rpnnen1lem3  10360  rpnnen1lem5  10362  dflt2  10498  fzval2  10801  fzof  10888  flval3  10961  uzsup  10983  uzrdgfni  11037  expcl2lem  11131  rpexpcl  11138  expge0  11154  expge1  11155  hashxrcl  11367  seqcoll  11417  wrdexg  11441  seqshft  11596  sqrlem3  11746  limsupval2  11970  limsupgre  11971  rlimpm  11990  rlimclim  12036  isercolllem1  12154  isercolllem2  12155  isercoll  12157  caurcvg  12165  caucvg  12167  summolem2a  12204  summolem2  12205  zsum  12207  fsumcvg3  12218  fsumrpcl  12226  fsumge0  12269  climfsum  12294  ackbijnn  12302  divalglem8  12615  sadaddlem  12673  isprm3  12783  maxprmfct  12808  pclem  12907  prmreclem1  12979  prmreclem2  12980  prmreclem3  12981  1arith  12990  4sqlem11  13018  ramtlecl  13063  ramcl2lem  13072  ramxrcl  13080  structfn  13177  strlemor1  13251  strleun  13254  srngbase  13280  srngplusg  13281  srngmulr  13282  lmodbase  13289  lmodplusg  13290  lmodsca  13291  algbase  13294  algaddg  13295  algmulr  13296  algsca  13297  algvsca  13298  phlbase  13304  phlplusg  13305  phlsca  13306  phlvsca  13307  phlip  13308  odrngbas  13328  odrngplusg  13329  odrngmulr  13330  odrngtset  13331  odrngle  13332  odrngds  13333  prdsval  13371  prdssca  13372  prdsbas  13373  prdsplusg  13374  prdsmulr  13375  prdsvsca  13376  prdsle  13377  prdsds  13379  prdstset  13381  prdshom  13382  prdsco  13383  imasbas  13431  imasds  13432  imasplusg  13436  imasmulr  13437  imassca  13438  imasvsca  13439  imastset  13440  imasle  13441  wunfunc  13789  fullfunc  13796  fthfunc  13797  isfull  13800  isfth  13804  wunnat  13846  dmcoass  13914  catcisolem  13954  catciso  13955  catcoppccl  13956  catcfuccl  13957  catcxpccl  13997  ipobas  14274  ipolerval  14275  ipotset  14276  psdmrn  14332  psss  14339  ledm  14362  lern  14363  dirdm  14372  dirge  14375  gexex  15161  gsumval3  15207  gsumzaddlem  15219  gsumconst  15225  gsumunsn  15237  lssacs  15740  asplss  16085  aspsubrg  16087  psrass1lem  16139  psrbas  16140  psrplusg  16142  psrmulr  16145  psrsca  16150  psrvscafval  16151  psrass1  16166  psrdi  16167  psrdir  16168  psrcom  16169  psrass23  16170  psropprmul  16332  coe1mul2  16362  cnfldbas  16399  cnfldadd  16400  cnfldmul  16401  cnfldcj  16402  cnfldtset  16403  cnfldle  16404  cnfldds  16405  zntoslem  16526  leordtval2  16958  lmbrf  17006  lmres  17044  fiuncmp  17147  1stckgenlem  17264  kgencn3  17269  ptbasfi  17292  xkoopn  17300  txcnmpt  17334  txkgen  17362  opnfbas  17553  fmfnfmlem4  17668  tsmsxplem1  17851  nmoffn  18236  nmofval  18239  nmogelb  18241  nmolb  18242  nmof  18244  qtopbas  18284  tgqioo  18322  re2ndc  18323  iitopon  18399  dfii3  18403  iimulcn  18452  xrhmeo  18460  cnheiborlem  18468  bndth  18472  lebnumii  18480  reparphti  18511  pcoass  18538  cphsqrcl  18636  lmmbrf  18704  iscauf  18722  caucfil  18725  lmclimf  18745  ovolfioo  18843  ovolficc  18844  ovolficcss  18845  ovolfsf  18847  ovollb  18854  ovolicc2lem3  18894  ovolicc2lem4  18895  ovolicc2  18897  volf  18904  volsup  18929  ovolfs2  18942  uniiccdif  18949  uniioovol  18950  uniiccvol  18951  uniioombllem2  18954  uniioombllem3a  18955  uniioombllem3  18956  uniioombllem4  18957  uniioombllem5  18958  uniioombl  18960  dyadmbllem  18970  dyadmbl  18971  opnmbllem  18972  opnmblALT  18974  volsup2  18976  vitalilem4  18982  vitalilem5  18983  vitali  18984  mbfimaopnlem  19026  mbflimsup  19037  i1f0  19058  i1f1  19061  itg11  19062  itg2mulc  19118  itg2gt0  19131  ellimc2  19243  limcresi  19251  dvreslem  19275  dvres2lem  19276  dvaddbr  19303  dvmulbr  19304  dvlipcn  19357  c1liplem1  19359  lhop1lem  19376  lhop1  19377  lhop2  19378  lhop  19379  dvfsumrlim  19394  ftc1cn  19406  itgsubstlem  19411  itgsubst  19412  mdegleb  19466  mdeglt  19467  mdegldg  19468  mdegxrcl  19469  mdegcl  19471  mdegaddle  19476  mdegmullem  19480  deg1mul3le  19518  ig1peu  19573  ig1pdvds  19578  aacjcl  19723  aannenlem2  19725  aannenlem3  19726  aalioulem2  19729  taylfval  19754  radcnvcl  19809  radcnvlt1  19810  radcnvle  19812  abelth  19833  abelth2  19834  pilem2  19844  pilem3  19845  pige3  19901  recosf1o  19913  resinf1o  19914  tanord1  19915  logcn  20010  dvlog  20014  dvlog2lem  20015  efopn  20021  logtayl  20023  cxpcn3  20104  loglesqr  20114  ssscongptld  20138  leibpi  20254  efrlim  20280  jensenlem1  20297  jensenlem2  20298  jensen  20299  amgm  20301  ftalem5  20330  efnnfsumcl  20356  efchtdvds  20413  dvdsmulf1o  20450  fsumdvdsmul  20451  lgsfcl2  20557  2sqlem6  20624  2sqlem8  20627  2sqlem9  20628  rpvmasumlem  20652  rpvmasum2  20677  dchrisum0re  20678  dchrisum0lem3  20684  dchrisum0  20685  rplogsum  20692  dirith2  20693  nmlno0lem  21387  hlimcaui  21832  chsspwh  21842  shsss  21908  chintcli  21926  shsleji  21965  shub1i  21969  shsval2i  21982  lejdii  22133  spanuni  22139  sshhococi  22141  spansnpji  22173  osumcori  22238  5oai  22256  3oalem6  22262  3oai  22263  pjssmii  22276  mayete3i  22323  mayete3iOLD  22324  mayetes3i  22325  nmlnop0iALT  22591  imaelshi  22654  pjnmopi  22744  pjclem1  22791  pjci  22796  mdslmd1lem1  22921  shatomistici  22957  hatomistici  22958  chpssati  22959  ballotlemfc0  23067  ballotlemfcc  23068  ballotlemiex  23076  ballotlemsup  23079  ballotlemsdom  23086  ballotlemsima  23090  ballotlemrv2  23096  ballotth  23112  xppreima  23226  fzossnn  23293  unitsscn  23295  xrsmulgzz  23322  xrge0iifhom  23334  fsumrp0cl  23349  iundisjfi  23378  iundisj2fi  23379  lmlimxrge0  23387  lmxrge0  23390  esumcst  23451  esumpfinvallem  23457  esumpfinval  23458  esumpfinvalf  23459  esumcvg  23469  imambfm  23582  elmbfmvol2  23587  subfacp1lem2a  23726  erdszelem4  23740  erdszelem5  23741  erdszelem7  23743  erdszelem8  23744  kur14lem7  23758  kur14lem9  23760  cvxpcon  23788  cvxscon  23789  rescon  23792  iccllyscon  23796  umgrass  23886  prodmolem2a  24157  prodmolem2  24158  zprod  24160  txpss3v  24489  txprel  24490  onint1  24960  itg2addnc  25005  ftc1cnnclem  25024  ftc1cnnc  25025  dvreasin  25026  dvreacos  25027  areacirclem2  25028  areacirclem3  25029  areacirclem4  25030  relded  25843  relcat  25864  lemindclsbu  26098  finminlem  26334  comppfsc  26410  tailf  26427  filnetlem3  26432  caures  26579  reheibor  26666  diophin  26955  4rexfrabdioph  26982  6rexfrabdioph  26983  irrapxlem1  27010  irrapx1  27016  monotuz  27129  jm2.27dlem5  27209  uvcff  27343  hbtlem2  27431  mvdco  27491  f1omvdconj  27492  lhe4.4ex1a  27649  itgsin0pilem1  27847  itgsinexp  27852  wallispilem2  27918  injresinj  28215  constr3pthlem1  28401  relopabVD  28993  bnj1145  29339  bnj1286  29365  atlatmstc  30131  atlatle  30132  pmaple  30572  sspadd1  30626  sspadd2  30627
This theorem was proved from axioms:  ax-1 5  ax-2 6  ax-3 7  ax-mp 8  ax-gen 1536  ax-5 1547  ax-17 1606  ax-9 1644  ax-8 1661  ax-6 1715  ax-7 1720  ax-11 1727  ax-12 1878  ax-ext 2277
This theorem depends on definitions:  df-bi 177  df-an 360  df-tru 1310  df-ex 1532  df-nf 1535  df-sb 1639  df-clab 2283  df-cleq 2289  df-clel 2292  df-in 3172  df-ss 3179
  Copyright terms: Public domain W3C validator