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

Theorem sstri 3317
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 3315 . 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 3280
This theorem is referenced by:  snsstp1  3909  snsstp2  3910  uniintsn  4047  dmexg  5089  rnexg  5090  ssrnres  5268  cossxp  5351  fabexg  5583  foimacnv  5651  ssimaex  5747  oprabss  6118  fparlem3  6407  fparlem4  6408  tposssxp  6442  riotassuni  6547  mapsspw  7008  sbthlem5  7180  sbthlem7  7182  marypha1lem  7396  ordtypelem4  7446  hartogslem1  7467  tc2  7637  tz9.12lem1  7669  rankval4  7749  rankxpl  7757  rankxplim  7759  infxpenlem  7851  ackbij1lem18  8073  cflm  8086  fin23lem29  8177  hsmexlem4  8265  hsmexlem5  8266  brdom3  8362  brdom5  8363  brdom4  8364  smobeth  8417  pwfseqlem3  8491  wundm  8559  wunrn  8560  wunex2  8569  ltsopi  8721  dmaddpi  8723  dmmulpi  8724  nqerf  8763  ltrelxr  9095  nnsscn  9961  nn0sscn  10182  uzwo2  10497  uzinfmi  10511  infmssuzle  10514  infmssuzcl  10515  uzwo3  10525  nn0ssq  10538  nnssq  10539  qsscn  10541  rpnnen1lem3  10558  rpnnen1lem5  10560  dflt2  10697  fzval2  11002  fzof  11092  fzossnn  11127  injresinj  11155  flval3  11177  uzsup  11199  uzrdgfni  11253  expcl2lem  11348  rpexpcl  11355  expge0  11371  expge1  11372  hashxrcl  11595  seqcoll  11667  wrdexg  11694  seqshft  11855  sqrlem3  12005  limsupval2  12229  limsupgre  12230  rlimpm  12249  rlimclim  12295  isercolllem1  12413  isercolllem2  12414  isercoll  12416  caurcvg  12425  caucvg  12427  summolem2a  12464  summolem2  12465  zsum  12467  fsumcvg3  12478  fsumrpcl  12486  fsumge0  12529  climfsum  12554  ackbijnn  12562  divalglem8  12875  sadaddlem  12933  isprm3  13043  maxprmfct  13068  pclem  13167  prmreclem1  13239  prmreclem2  13240  prmreclem3  13241  1arith  13250  4sqlem11  13278  ramtlecl  13323  ramcl2lem  13332  ramxrcl  13340  structfn  13437  strlemor1  13511  strleun  13514  srngbase  13540  srngplusg  13541  srngmulr  13542  lmodbase  13549  lmodplusg  13550  lmodsca  13551  algbase  13554  algaddg  13555  algmulr  13556  algsca  13557  algvsca  13558  phlbase  13564  phlplusg  13565  phlsca  13566  phlvsca  13567  phlip  13568  odrngbas  13590  odrngplusg  13591  odrngmulr  13592  odrngtset  13593  odrngle  13594  odrngds  13595  prdsval  13633  prdssca  13634  prdsbas  13635  prdsplusg  13636  prdsmulr  13637  prdsvsca  13638  prdsle  13639  prdsds  13641  prdstset  13643  prdshom  13644  prdsco  13645  imasbas  13693  imasds  13694  imasplusg  13698  imasmulr  13699  imassca  13700  imasvsca  13701  imastset  13702  imasle  13703  wunfunc  14051  fullfunc  14058  fthfunc  14059  isfull  14062  isfth  14066  wunnat  14108  dmcoass  14176  catcisolem  14216  catciso  14217  catcoppccl  14218  catcfuccl  14219  catcxpccl  14259  ipobas  14536  ipolerval  14537  ipotset  14538  psdmrn  14594  psss  14601  ledm  14624  lern  14625  dirdm  14634  dirge  14637  gexex  15423  gsumval3  15469  gsumzaddlem  15481  gsumconst  15487  gsumunsn  15499  lssacs  15998  asplss  16343  aspsubrg  16345  psrass1lem  16397  psrbas  16398  psrplusg  16400  psrmulr  16403  psrsca  16408  psrvscafval  16409  psrass1  16424  psrdi  16425  psrdir  16426  psrcom  16427  psrass23  16428  psropprmul  16587  coe1mul2  16617  cnfldbas  16662  cnfldadd  16663  cnfldmul  16664  cnfldcj  16665  cnfldtset  16666  cnfldle  16667  cnfldds  16668  cnfldunif  16669  zntoslem  16792  leordtval2  17230  lmbrf  17278  lmres  17318  fiuncmp  17421  1stckgenlem  17538  kgencn3  17543  ptbasfi  17566  xkoopn  17574  txcnmpt  17609  txkgen  17637  opnfbas  17827  fmfnfmlem4  17942  tsmsxplem1  18135  trust  18212  restutop  18220  nmoffn  18698  nmofval  18701  nmogelb  18703  nmolb  18704  nmof  18706  qtopbas  18746  tgqioo  18784  re2ndc  18785  iitopon  18862  dfii3  18866  iimulcn  18916  cnheiborlem  18932  bndth  18936  lebnumii  18944  reparphti  18975  pcoass  19002  cphsqrcl  19100  lmmbrf  19168  iscauf  19186  caucfil  19189  lmclimf  19209  ovolfioo  19317  ovolficc  19318  ovolficcss  19319  ovolfsf  19321  ovollb  19328  ovolicc2lem3  19368  ovolicc2lem4  19369  ovolicc2  19371  volf  19378  volsup  19403  ovolfs2  19416  uniiccdif  19423  uniioovol  19424  uniiccvol  19425  uniioombllem2  19428  uniioombllem3a  19429  uniioombllem3  19430  uniioombllem4  19431  uniioombllem5  19432  uniioombl  19434  dyadmbllem  19444  dyadmbl  19445  opnmbllem  19446  opnmblALT  19448  volsup2  19450  vitalilem4  19456  vitalilem5  19457  vitali  19458  mbfimaopnlem  19500  mbflimsup  19511  i1f0  19532  i1f1  19535  itg11  19536  itg2mulc  19592  itg2gt0  19605  ellimc2  19717  limcresi  19725  dvreslem  19749  dvres2lem  19750  dvaddbr  19777  dvmulbr  19778  dvlipcn  19831  c1liplem1  19833  lhop1lem  19850  lhop1  19851  lhop2  19852  lhop  19853  dvfsumrlim  19868  ftc1cn  19880  itgsubstlem  19885  itgsubst  19886  mdegleb  19940  mdeglt  19941  mdegldg  19942  mdegxrcl  19943  mdegcl  19945  mdegaddle  19950  mdegmullem  19954  deg1mul3le  19992  ig1peu  20047  ig1pdvds  20052  aacjcl  20197  aannenlem2  20199  aannenlem3  20200  aalioulem2  20203  taylfval  20228  radcnvcl  20286  radcnvlt1  20287  radcnvle  20289  abelth  20310  abelth2  20311  pilem2  20321  pilem3  20322  pige3  20378  recosf1o  20390  resinf1o  20391  tanord1  20392  logcn  20491  dvlog  20495  dvlog2lem  20496  efopn  20502  logtayl  20504  cxpcn3  20585  loglesqr  20595  ssscongptld  20619  leibpi  20735  efrlim  20761  jensenlem1  20778  jensenlem2  20779  jensen  20780  amgm  20782  ftalem5  20812  efnnfsumcl  20838  efchtdvds  20895  dvdsmulf1o  20932  fsumdvdsmul  20933  lgsfcl2  21039  2sqlem6  21106  2sqlem8  21109  2sqlem9  21110  rpvmasumlem  21134  rpvmasum2  21159  dchrisum0re  21160  dchrisum0lem3  21166  dchrisum0  21167  rplogsum  21174  dirith2  21175  umgrass  21307  constr3pthlem1  21595  nmlno0lem  22247  hlimcaui  22692  chsspwh  22702  shsss  22768  chintcli  22786  shsleji  22825  shub1i  22829  shsval2i  22842  lejdii  22993  spanuni  22999  sshhococi  23001  spansnpji  23033  osumcori  23098  5oai  23116  3oalem6  23122  3oai  23123  pjssmii  23136  mayete3i  23183  mayete3iOLD  23184  mayetes3i  23185  nmlnop0iALT  23451  imaelshi  23514  pjnmopi  23604  pjclem1  23651  pjci  23656  mdslmd1lem1  23781  shatomistici  23817  hatomistici  23818  chpssati  23819  xppreima  24012  iundisjfi  24105  iundisj2fi  24106  xrsmulgzz  24153  fsumrp0cl  24170  unitsscn  24247  xrge0iifhom  24276  lmlimxrge0  24287  lmxrge0  24290  esumcst  24408  esumpfinvallem  24417  esumpfinval  24418  esumpfinvalf  24419  esumcvg  24429  measunl  24523  imambfm  24565  elmbfmvol2  24570  sxbrsigalem3  24575  sxbrsigalem2  24589  sxbrsigalem4  24590  sitgclg  24609  ballotlemfc0  24703  ballotlemfcc  24704  ballotlemiex  24712  ballotlemsup  24715  ballotlemsdom  24722  ballotlemsima  24726  ballotlemrv2  24732  ballotth  24748  lgamgulmlem2  24767  subfacp1lem2a  24819  erdszelem4  24833  erdszelem5  24834  erdszelem7  24836  erdszelem8  24837  kur14lem7  24851  kur14lem9  24853  cvxpcon  24882  cvxscon  24883  rescon  24886  iccllyscon  24890  prodmolem2a  25213  prodmolem2  25214  zprod  25216  fprodrpcl  25235  rprisefaccl  25291  txpss3v  25632  txprel  25633  onint1  26103  mblfinlem  26143  mblfinlem2  26144  mblfinlem3  26145  ismblfin  26146  mbfposadd  26153  cnambfre  26154  itg2addnc  26158  ftc1cnnclem  26177  ftc1cnnc  26178  dvreasin  26179  dvreacos  26180  areacirclem2  26181  areacirclem3  26182  areacirclem4  26183  finminlem  26211  comppfsc  26277  tailf  26294  filnetlem3  26299  caures  26356  reheibor  26438  diophin  26721  4rexfrabdioph  26748  6rexfrabdioph  26749  irrapxlem1  26775  irrapx1  26781  monotuz  26894  jm2.27dlem5  26974  uvcff  27108  hbtlem2  27196  mvdco  27256  f1omvdconj  27257  lhe4.4ex1a  27414  itgsin0pilem1  27611  itgsinexplem1  27615  itgsinexp  27616  wallispilem2  27682  relopabVD  28722  bnj1145  29068  bnj1286  29094  atlatmstc  29802  atlatle  29803  pmaple  30243  sspadd1  30297  sspadd2  30298
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 2385
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 2391  df-cleq 2397  df-clel 2400  df-in 3287  df-ss 3294
  Copyright terms: Public domain W3C validator