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

Theorem sstri 3293
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 3291 . 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 3256
This theorem is referenced by:  snsstp1  3885  snsstp2  3886  uniintsn  4022  dmexg  5063  rnexg  5064  ssrnres  5242  cossxp  5325  fabexg  5557  foimacnv  5625  ssimaex  5720  oprabss  6091  fparlem3  6380  fparlem4  6381  tposssxp  6412  riotassuni  6517  mapsspw  6978  sbthlem5  7150  sbthlem7  7152  marypha1lem  7366  ordtypelem4  7416  hartogslem1  7437  tc2  7607  tz9.12lem1  7639  rankval4  7719  rankxpl  7727  rankxplim  7729  infxpenlem  7821  ackbij1lem18  8043  cflm  8056  fin23lem29  8147  hsmexlem4  8235  hsmexlem5  8236  brdom3  8332  brdom5  8333  brdom4  8334  smobeth  8387  pwfseqlem3  8461  wundm  8529  wunrn  8530  wunex2  8539  ltsopi  8691  dmaddpi  8693  dmmulpi  8694  nqerf  8733  ltrelxr  9065  nnsscn  9930  nn0sscn  10151  uzwo2  10466  uzinfmi  10480  infmssuzle  10483  infmssuzcl  10484  uzwo3  10494  nn0ssq  10507  nnssq  10508  qsscn  10510  rpnnen1lem3  10527  rpnnen1lem5  10529  dflt2  10666  fzval2  10971  fzof  11060  injresinj  11120  flval3  11142  uzsup  11164  uzrdgfni  11218  expcl2lem  11313  rpexpcl  11320  expge0  11336  expge1  11337  hashxrcl  11560  seqcoll  11632  wrdexg  11659  seqshft  11820  sqrlem3  11970  limsupval2  12194  limsupgre  12195  rlimpm  12214  rlimclim  12260  isercolllem1  12378  isercolllem2  12379  isercoll  12381  caurcvg  12390  caucvg  12392  summolem2a  12429  summolem2  12430  zsum  12432  fsumcvg3  12443  fsumrpcl  12451  fsumge0  12494  climfsum  12519  ackbijnn  12527  divalglem8  12840  sadaddlem  12898  isprm3  13008  maxprmfct  13033  pclem  13132  prmreclem1  13204  prmreclem2  13205  prmreclem3  13206  1arith  13215  4sqlem11  13243  ramtlecl  13288  ramcl2lem  13297  ramxrcl  13305  structfn  13402  strlemor1  13476  strleun  13479  srngbase  13505  srngplusg  13506  srngmulr  13507  lmodbase  13514  lmodplusg  13515  lmodsca  13516  algbase  13519  algaddg  13520  algmulr  13521  algsca  13522  algvsca  13523  phlbase  13529  phlplusg  13530  phlsca  13531  phlvsca  13532  phlip  13533  odrngbas  13555  odrngplusg  13556  odrngmulr  13557  odrngtset  13558  odrngle  13559  odrngds  13560  prdsval  13598  prdssca  13599  prdsbas  13600  prdsplusg  13601  prdsmulr  13602  prdsvsca  13603  prdsle  13604  prdsds  13606  prdstset  13608  prdshom  13609  prdsco  13610  imasbas  13658  imasds  13659  imasplusg  13663  imasmulr  13664  imassca  13665  imasvsca  13666  imastset  13667  imasle  13668  wunfunc  14016  fullfunc  14023  fthfunc  14024  isfull  14027  isfth  14031  wunnat  14073  dmcoass  14141  catcisolem  14181  catciso  14182  catcoppccl  14183  catcfuccl  14184  catcxpccl  14224  ipobas  14501  ipolerval  14502  ipotset  14503  psdmrn  14559  psss  14566  ledm  14589  lern  14590  dirdm  14599  dirge  14602  gexex  15388  gsumval3  15434  gsumzaddlem  15446  gsumconst  15452  gsumunsn  15464  lssacs  15963  asplss  16308  aspsubrg  16310  psrass1lem  16362  psrbas  16363  psrplusg  16365  psrmulr  16368  psrsca  16373  psrvscafval  16374  psrass1  16389  psrdi  16390  psrdir  16391  psrcom  16392  psrass23  16393  psropprmul  16552  coe1mul2  16582  cnfldbas  16623  cnfldadd  16624  cnfldmul  16625  cnfldcj  16626  cnfldtset  16627  cnfldle  16628  cnfldds  16629  cnfldunif  16630  zntoslem  16753  leordtval2  17191  lmbrf  17239  lmres  17279  fiuncmp  17382  1stckgenlem  17499  kgencn3  17504  ptbasfi  17527  xkoopn  17535  txcnmpt  17570  txkgen  17598  opnfbas  17788  fmfnfmlem4  17903  tsmsxplem1  18096  trust  18173  restutop  18181  nmoffn  18609  nmofval  18612  nmogelb  18614  nmolb  18615  nmof  18617  qtopbas  18657  tgqioo  18695  re2ndc  18696  iitopon  18773  dfii3  18777  iimulcn  18827  cnheiborlem  18843  bndth  18847  lebnumii  18855  reparphti  18886  pcoass  18913  cphsqrcl  19011  lmmbrf  19079  iscauf  19097  caucfil  19100  lmclimf  19120  ovolfioo  19224  ovolficc  19225  ovolficcss  19226  ovolfsf  19228  ovollb  19235  ovolicc2lem3  19275  ovolicc2lem4  19276  ovolicc2  19278  volf  19285  volsup  19310  ovolfs2  19323  uniiccdif  19330  uniioovol  19331  uniiccvol  19332  uniioombllem2  19335  uniioombllem3a  19336  uniioombllem3  19337  uniioombllem4  19338  uniioombllem5  19339  uniioombl  19341  dyadmbllem  19351  dyadmbl  19352  opnmbllem  19353  opnmblALT  19355  volsup2  19357  vitalilem4  19363  vitalilem5  19364  vitali  19365  mbfimaopnlem  19407  mbflimsup  19418  i1f0  19439  i1f1  19442  itg11  19443  itg2mulc  19499  itg2gt0  19512  ellimc2  19624  limcresi  19632  dvreslem  19656  dvres2lem  19657  dvaddbr  19684  dvmulbr  19685  dvlipcn  19738  c1liplem1  19740  lhop1lem  19757  lhop1  19758  lhop2  19759  lhop  19760  dvfsumrlim  19775  ftc1cn  19787  itgsubstlem  19792  itgsubst  19793  mdegleb  19847  mdeglt  19848  mdegldg  19849  mdegxrcl  19850  mdegcl  19852  mdegaddle  19857  mdegmullem  19861  deg1mul3le  19899  ig1peu  19954  ig1pdvds  19959  aacjcl  20104  aannenlem2  20106  aannenlem3  20107  aalioulem2  20110  taylfval  20135  radcnvcl  20193  radcnvlt1  20194  radcnvle  20196  abelth  20217  abelth2  20218  pilem2  20228  pilem3  20229  pige3  20285  recosf1o  20297  resinf1o  20298  tanord1  20299  logcn  20398  dvlog  20402  dvlog2lem  20403  efopn  20409  logtayl  20411  cxpcn3  20492  loglesqr  20502  ssscongptld  20526  leibpi  20642  efrlim  20668  jensenlem1  20685  jensenlem2  20686  jensen  20687  amgm  20689  ftalem5  20719  efnnfsumcl  20745  efchtdvds  20802  dvdsmulf1o  20839  fsumdvdsmul  20840  lgsfcl2  20946  2sqlem6  21013  2sqlem8  21016  2sqlem9  21017  rpvmasumlem  21041  rpvmasum2  21066  dchrisum0re  21067  dchrisum0lem3  21073  dchrisum0  21074  rplogsum  21081  dirith2  21082  umgrass  21214  constr3pthlem1  21483  nmlno0lem  22135  hlimcaui  22580  chsspwh  22590  shsss  22656  chintcli  22674  shsleji  22713  shub1i  22717  shsval2i  22730  lejdii  22881  spanuni  22887  sshhococi  22889  spansnpji  22921  osumcori  22986  5oai  23004  3oalem6  23010  3oai  23011  pjssmii  23024  mayete3i  23071  mayete3iOLD  23072  mayetes3i  23073  nmlnop0iALT  23339  imaelshi  23402  pjnmopi  23492  pjclem1  23539  pjci  23544  mdslmd1lem1  23669  shatomistici  23705  hatomistici  23706  chpssati  23707  xppreima  23894  fzossnn  23981  iundisjfi  23983  iundisj2fi  23984  xrsmulgzz  24026  fsumrp0cl  24039  unitsscn  24091  xrge0iifhom  24120  lmlimxrge0  24131  lmxrge0  24134  esumcst  24244  esumpfinvallem  24253  esumpfinval  24254  esumpfinvalf  24255  esumcvg  24265  measunl  24357  imambfm  24399  elmbfmvol2  24404  sxbrsigalem3  24409  sxbrsigalem2  24423  sxbrsigalem4  24424  ballotlemfc0  24522  ballotlemfcc  24523  ballotlemiex  24531  ballotlemsup  24534  ballotlemsdom  24541  ballotlemsima  24545  ballotlemrv2  24551  ballotth  24567  lgamgulmlem2  24586  subfacp1lem2a  24638  erdszelem4  24652  erdszelem5  24653  erdszelem7  24655  erdszelem8  24656  kur14lem7  24670  kur14lem9  24672  cvxpcon  24701  cvxscon  24702  rescon  24705  iccllyscon  24709  prodmolem2a  25032  prodmolem2  25033  zprod  25035  fprodrpcl  25054  rprisefaccl  25100  txpss3v  25435  txprel  25436  onint1  25906  itg2addnc  25952  ftc1cnnclem  25971  ftc1cnnc  25972  dvreasin  25973  dvreacos  25974  areacirclem2  25975  areacirclem3  25976  areacirclem4  25977  finminlem  26005  comppfsc  26071  tailf  26088  filnetlem3  26093  caures  26150  reheibor  26232  diophin  26515  4rexfrabdioph  26542  6rexfrabdioph  26543  irrapxlem1  26569  irrapx1  26575  monotuz  26688  jm2.27dlem5  26768  uvcff  26902  hbtlem2  26990  mvdco  27050  f1omvdconj  27051  lhe4.4ex1a  27208  itgsin0pilem1  27405  itgsinexplem1  27409  itgsinexp  27410  wallispilem2  27476  relopabVD  28347  bnj1145  28693  bnj1286  28719  atlatmstc  29485  atlatle  29486  pmaple  29926  sspadd1  29980  sspadd2  29981
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 1661  ax-8 1682  ax-6 1736  ax-7 1741  ax-11 1753  ax-12 1939  ax-ext 2361
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 2367  df-cleq 2373  df-clel 2376  df-in 3263  df-ss 3270
  Copyright terms: Public domain W3C validator