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

Theorem sstri 3470
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 3468 . 2  |-  ( A 
C_  B  ->  ( B  C_  C  ->  A  C_  C ) )
41, 2, 3mp2 9 1  |-  A  C_  C
Colors of variables: wff setvar class
Syntax hints:    C_ wss 3433
This theorem was proved from axioms:  ax-mp 5  ax-1 6  ax-2 7  ax-3 8  ax-gen 1665  ax-4 1678  ax-5 1748  ax-6 1794  ax-7 1838  ax-10 1886  ax-11 1891  ax-12 1904  ax-13 2052  ax-ext 2398
This theorem depends on definitions:  df-bi 188  df-an 372  df-tru 1440  df-ex 1660  df-nf 1664  df-sb 1787  df-clab 2406  df-cleq 2412  df-clel 2415  df-in 3440  df-ss 3447
This theorem is referenced by:  snsstp1  4145  snsstp2  4146  uniintsn  4287  ssrnres  5286  cossxp  5369  foimacnv  5839  ssimaex  5937  riotassuni  6294  oprabss  6387  dmexg  6729  rnexg  6730  fabexg  6754  fparlem3  6900  fparlem4  6901  snopsuppss  6931  tposssxp  6976  mapsspw  7506  sbthlem5  7683  sbthlem7  7685  cnvimamptfin  7872  marypha1lem  7944  ordtypelem4  8027  hartogslem1  8048  tc2  8216  tz9.12lem1  8248  rankval4  8328  rankxpl  8336  rankmapu  8339  rankxplim  8340  infxpenlem  8434  ackbij1lem18  8656  cflm  8669  fin23lem29  8760  hsmexlem4  8848  hsmexlem5  8849  brdom3  8945  brdom5  8946  brdom4  8947  smobeth  9000  pwfseqlem3  9074  wundm  9142  wunrn  9143  wunex2  9152  ltsopi  9302  dmaddpi  9304  dmmulpi  9305  nqerf  9344  ltrelxr  9684  nnsscn  10603  nn0sscn  10863  uzwo2  11212  uzinfmiOLD  11228  infssuzle  11233  infssuzcl  11234  infmssuzleOLD  11235  infmssuzclOLD  11236  uzwo3  11248  nn0ssq  11261  nnssq  11262  qsscn  11264  rpnnen1lem3  11281  rpnnen1lem5  11283  dflt2  11436  fzval2  11774  fzof  11904  fzossnn  11950  fzo0ssnn0  11980  injresinj  12011  flval3  12036  uzsup  12076  uzrdgfni  12158  expcl2lem  12270  rpexpcl  12277  expge0  12294  expge1  12295  hashxrcl  12525  seqcoll  12610  wrdexg  12658  xptrrel  13012  trclublem  13027  sqrlem3  13276  limsupval2  13507  limsupval2OLD  13508  limsupgre  13509  limsupgreOLD  13510  rlimpm  13531  rlimclim  13577  isercolllem1  13695  isercolllem2  13696  isercoll  13698  caurcvg  13709  caurcvgOLD  13710  caucvg  13712  summolem2a  13748  summolem2  13749  zsum  13751  fsumcvg3  13762  fsumrpcl  13770  fsumge0  13822  climfsum  13847  ackbijnn  13853  prodmolem2a  13955  prodmolem2  13956  zprod  13958  fprodrpcl  13977  fprodge0  14014  fprodge1  14016  rprisefaccl  14043  divalglem8  14345  sadaddlem  14403  lcmfval  14551  lcmfvalOLD  14555  isprm3  14593  maxprmfct  14612  pclem  14740  prmreclem1  14812  prmreclem2  14813  prmreclem3  14814  1arith  14823  4sqlem11  14851  ramtlecl  14903  ramcl2lem  14914  ramcl2lemOLD  14915  ramxrcl  14927  prmgaplem3  14975  prmgaplem4  14976  cshwshashlem1  15018  structfn  15086  strlemor1  15169  strleun  15172  srngbase  15205  srngplusg  15206  srngmulr  15207  lmodbase  15214  lmodplusg  15215  lmodsca  15216  ipsbase  15221  ipsaddg  15222  ipsmulr  15223  ipssca  15224  ipsvsca  15225  ipsip  15226  phlbase  15231  phlplusg  15232  phlsca  15233  phlvsca  15234  phlip  15235  odrngbas  15257  odrngplusg  15258  odrngmulr  15259  odrngtset  15260  odrngle  15261  odrngds  15262  prdsval  15305  prdssca  15306  prdsbas  15307  prdsplusg  15308  prdsmulr  15309  prdsvsca  15310  prdsip  15311  prdsle  15312  prdsds  15314  prdstset  15316  prdshom  15317  prdsco  15318  imasbas  15362  imasds  15363  imasplusg  15367  imasmulr  15368  imassca  15369  imasvsca  15370  imasip  15371  imastset  15372  imasle  15373  wunfunc  15748  fullfunc  15755  fthfunc  15756  isfull  15759  isfth  15763  wunnat  15805  dmcoass  15905  catcisolem  15945  catciso  15946  catcoppccl  15947  catcfuccl  15948  catcxpccl  16036  ipobas  16345  ipolerval  16346  ipotset  16347  psdmrn  16397  psss  16404  ledm  16414  lern  16415  dirdm  16424  dirge  16427  mvdco  17030  f1omvdconj  17031  gexex  17419  gsumval3  17469  lssacs  18118  asplss  18481  aspsubrg  18483  psrass1lem  18529  psrbas  18530  psrplusg  18533  psrmulr  18536  psrsca  18541  psrvscafval  18542  psrass1  18557  psrass23l  18560  psrcom  18561  psrass23  18562  psropprmul  18759  coe1mul2  18790  cnfldbas  18902  cnfldadd  18903  cnfldmul  18904  cnfldcj  18905  cnfldtset  18906  cnfldle  18907  cnfldds  18908  cnfldunif  18909  rge0srg  18965  zntoslem  19051  ofco2  19400  leordtval2  20152  lmbrf  20200  lmres  20240  fiuncmp  20343  comppfsc  20471  1stckgenlem  20492  kgencn3  20497  ptbasfi  20520  xkoopn  20528  txcnmpt  20563  txkgen  20591  opnfbas  20781  fmfnfmlem4  20896  tsmsxplem1  21091  trust  21168  restutop  21176  nmoffn  21636  nmofval  21639  nmogelb  21641  nmolb  21642  nmof  21644  qtopbas  21684  tgqioo  21722  re2ndc  21723  iitopon  21800  dfii3  21804  iimulcn  21855  cnheiborlem  21871  bndth  21875  lebnumii  21883  reparphti  21914  pcoass  21941  cphsqrtcl  22048  lmmbrf  22118  iscauf  22136  caucfil  22139  lmclimf  22159  rrxmval  22245  rrxmet  22248  ovolfioo  22294  ovolficc  22295  ovolficcss  22296  ovolfsf  22298  ovollb  22306  ovolicc2lem3  22346  ovolicc2lem4OLD  22347  ovolicc2lem4  22348  ovolicc2  22350  volf  22357  volsup  22383  ovolfs2  22397  uniiccdif  22409  uniioovol  22410  uniiccvol  22411  uniioombllem2  22414  uniioombllem2OLD  22415  uniioombllem3a  22416  uniioombllem3  22417  uniioombllem4  22418  uniioombllem5  22419  uniioombl  22421  dyadmbllem  22431  dyadmbl  22432  opnmbllem  22433  opnmblALT  22435  volsup2  22437  vitalilem4  22443  vitalilem5  22444  vitali  22445  mbfimaopnlem  22485  mbflimsup  22497  mbflimsupOLD  22498  i1f0  22519  i1f1  22522  itg11  22523  itg2mulc  22579  itg2gt0  22592  ellimc2  22706  limcresi  22714  dvreslem  22738  dvres2lem  22739  dvaddbr  22766  dvmulbr  22767  dvlipcn  22820  c1liplem1  22822  lhop1lem  22839  lhop1  22840  lhop2  22841  lhop  22842  dvfsumrlim  22857  ftc1cn  22869  itgsubstlem  22874  itgsubst  22875  mdegleb  22887  mdeglt  22888  mdegldg  22889  mdegxrcl  22890  mdegcl  22892  mdegaddle  22897  mdegmullem  22901  deg1mul3le  22939  ig1peu  22994  ig1pdvds  22999  aacjcl  23145  aannenlem2  23147  aannenlem3  23148  aalioulem2  23151  taylfval  23176  radcnvcl  23234  radcnvlt1  23235  radcnvle  23237  abelth  23258  abelth2  23259  pilem2  23269  pilem2OLD  23270  pilem3  23271  pilem3OLD  23272  pige3  23334  recosf1o  23346  resinf1o  23347  tanord1  23348  logcn  23454  dvlog  23458  dvlog2lem  23459  efopn  23465  logtayl  23467  cxpcn3  23550  loglesqrt  23560  ssscongptld  23613  leibpi  23730  efrlim  23757  jensenlem1  23774  jensenlem2  23775  jensen  23776  amgm  23778  lgamgulmlem2  23817  ftalem5  23863  efnnfsumcl  23889  efchtdvds  23946  dvdsmulf1o  23983  fsumdvdsmul  23984  lgsfcl2  24090  2sqlem6  24157  2sqlem8  24160  2sqlem9  24161  rpvmasumlem  24185  rpvmasum2  24210  dchrisum0re  24211  dchrisum0lem3  24217  dchrisum0  24218  rplogsum  24225  dirith2  24226  axtgcgrrflx  24370  axtgcgrid  24371  axtgsegcon  24372  axtg5seg  24373  axtgbtwnid  24374  axtgpasch  24375  axtgcont1  24376  motcgrg  24446  tglng  24448  umgrass  24889  constr3pthlem1  25225  disjxwwlkn  25315  nmlno0lem  26276  hlimcaui  26721  chsspwh  26732  shsss  26798  chintcli  26816  shsleji  26855  shub1i  26859  shsval2i  26872  lejdii  27023  spanuni  27029  sshhococi  27031  spansnpji  27063  osumcori  27128  5oai  27146  3oalem6  27152  3oai  27153  pjssmii  27166  mayete3i  27213  mayetes3i  27214  nmlnop0iALT  27480  imaelshi  27543  pjnmopi  27633  pjclem1  27680  pjci  27685  mdslmd1lem1  27810  shatomistici  27846  hatomistici  27847  chpssati  27848  xppreima  28085  iundisjfi  28205  iundisj2fi  28206  xrsmulgzz  28274  fsumrp0cl  28293  gsummpt2co  28378  xrge0slmod  28443  unitsscn  28538  ordtconlem1  28566  xrge0iifhom  28579  lmlimxrge0  28590  lmxrge0  28594  esumcst  28720  esumpfinvallem  28731  esumpfinval  28732  esumpfinvalf  28733  esumcvg  28743  imambfm  28920  elmbfmvol2  28925  sxbrsigalem3  28930  sxbrsigalem2  28944  sxbrsigalem4  28945  sitgclg  29000  eulerpartlem1  29023  eulerpartlemgvv  29032  eulerpartlemgh  29034  eulerpartlemgf  29035  ballotlemfc0  29148  ballotlemfcc  29149  ballotlemiex  29157  ballotlemsup  29160  ballotlemsdom  29167  ballotlemsima  29171  ballotlemrv2  29177  ballotth  29193  signsplypnf  29224  signsply0  29225  bnj1145  29587  bnj1286  29613  subfacp1lem2a  29688  erdszelem4  29702  erdszelem5  29703  erdszelem7  29705  erdszelem8  29706  kur14lem7  29720  kur14lem9  29722  cvxpcon  29750  cvxscon  29751  rescon  29754  iccllyscon  29758  txpss3v  30427  txprel  30428  limitssson  30460  finminlem  30756  tailf  30813  filnetlem3  30818  onint1  30891  bj-unrab  31276  bj-2upln1upl  31364  bj-rrvecsscmn  31449  taupilem2  31465  taupi  31466  poimirlem3  31647  poimirlem30  31674  poimirlem31  31675  poimirlem32  31676  broucube  31678  opnmbllem0  31680  mblfinlem1  31681  mblfinlem2  31682  mblfinlem3  31683  mblfinlem4  31684  ismblfin  31685  mbfposadd  31692  cnambfre  31693  itg2addnc  31700  ftc1cnnclem  31719  ftc1cnnc  31720  ftc1anclem3  31723  ftc1anclem7  31727  ftc1anc  31729  ftc2nc  31730  dvreasin  31734  dvreacos  31735  areacirclem1  31736  areacirclem2  31737  areacirc  31741  caures  31793  reheibor  31875  atlatmstc  32594  atlatle  32595  pmaple  33035  sspadd1  33089  sspadd2  33090  diophin  35324  4rexfrabdioph  35350  6rexfrabdioph  35351  irrapxlem1  35376  irrapx1  35382  monotuz  35499  jm2.27dlem5  35578  hbtlem2  35693  algbase  35747  algaddg  35748  algmulr  35749  algsca  35750  algvsca  35751  itgpowd  35802  arearect  35803  areaquad  35804  trrelsuperrel2dg  35906  relexpaddss  35953  brtrclfv2  35962  frege131d  35999  xphe  36017  idhe  36024  lhe4.4ex1a  36319  uzmptshftfval  36336  binomcxplemdvbinom  36343  binomcxplemcvg  36344  binomcxplemnotnn0  36346  relopabVD  36942  fzisoeu  37131  fzsscn  37144  fzssre  37148  ioosscn  37180  limcresiooub  37299  limcresioolb  37300  limcleqr  37301  limclner  37308  limclr  37312  icccncfext  37341  cncficcgt0  37342  ioodvbdlimc1lem2  37380  ioodvbdlimc2lem  37382  dvnprodlem1  37394  dvnprodlem2  37395  itgsin0pilem1  37399  itgsinexplem1  37403  itgsinexp  37404  dirkercncflem2  37539  fourierdlem16  37558  fourierdlem18  37560  fourierdlem20  37562  fourierdlem21  37563  fourierdlem22  37564  fourierdlem25  37567  fourierdlem37  37579  fourierdlem42  37584  fourierdlem50  37592  fourierdlem52  37594  fourierdlem62  37604  fourierdlem64  37606  fourierdlem66  37608  fourierdlem68  37610  fourierdlem74  37616  fourierdlem75  37617  fourierdlem76  37618  fourierdlem79  37621  fourierdlem83  37625  fourierdlem95  37637  fourierdlem101  37643  fourierdlem102  37644  fourierdlem103  37645  fourierdlem104  37646  fourierdlem112  37654  fourierdlem114  37656  sqwvfoura  37664  sqwvfourb  37665  fouriersw  37667  etransclem24  37694  etransclem48  37718  sge0sn  37759  sge0tsms  37760  sge0f1o  37762  sge0pr  37774  sge0resplit  37786  sge0split  37789  sge0iunmptlemre  37795  carageniuncllem1  37855  oddibas  38584  2zrngbas  38707  2zrng0  38709  aacllem  39314
  Copyright terms: Public domain W3C validator