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

Theorem sstri 3360
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 3358 . 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 3323
This theorem was proved from axioms:  ax-mp 5  ax-1 6  ax-2 7  ax-3 8  ax-gen 1591  ax-4 1602  ax-5 1670  ax-6 1708  ax-7 1728  ax-10 1775  ax-11 1780  ax-12 1792  ax-13 1943  ax-ext 2419
This theorem depends on definitions:  df-bi 185  df-an 371  df-ex 1587  df-nf 1590  df-sb 1701  df-clab 2425  df-cleq 2431  df-clel 2434  df-in 3330  df-ss 3337
This theorem is referenced by:  snsstp1  4019  snsstp2  4020  uniintsn  4160  ssrnres  5271  cossxp  5355  foimacnv  5653  ssimaex  5751  riotassuniOLD  6084  oprabss  6171  dmexg  6504  rnexg  6505  fabexg  6528  fparlem3  6669  fparlem4  6670  snopsuppss  6700  tposssxp  6744  mapsspw  7240  sbthlem5  7417  sbthlem7  7419  cnvimamptfin  7604  marypha1lem  7675  ordtypelem4  7727  hartogslem1  7748  tc2  7954  tz9.12lem1  7986  rankval4  8066  rankxpl  8074  rankmapu  8077  rankxplim  8078  infxpenlem  8172  ackbij1lem18  8398  cflm  8411  fin23lem29  8502  hsmexlem4  8590  hsmexlem5  8591  brdom3  8687  brdom5  8688  brdom4  8689  smobeth  8742  pwfseqlem3  8819  wundm  8887  wunrn  8888  wunex2  8897  ltsopi  9049  dmaddpi  9051  dmmulpi  9052  nqerf  9091  ltrelxr  9430  nnsscn  10319  nn0sscn  10576  uzwo2  10911  uzinfmi  10926  infmssuzle  10929  infmssuzcl  10930  uzwo3  10940  nn0ssq  10953  nnssq  10954  qsscn  10956  rpnnen1lem3  10973  rpnnen1lem5  10975  dflt2  11117  fzval2  11432  fzof  11542  fzossnn  11586  fzo0ssnn0  11603  injresinj  11631  flval3  11655  uzsup  11694  uzrdgfni  11773  expcl2lem  11869  rpexpcl  11876  expge0  11892  expge1  11893  hashxrcl  12119  seqcoll  12208  wrdexg  12236  seqshft  12566  sqrlem3  12726  limsupval2  12950  limsupgre  12951  rlimpm  12970  rlimclim  13016  isercolllem1  13134  isercolllem2  13135  isercoll  13137  caurcvg  13146  caucvg  13148  summolem2a  13184  summolem2  13185  zsum  13187  fsumcvg3  13198  fsumrpcl  13206  fsumge0  13250  climfsum  13275  ackbijnn  13283  divalglem8  13596  sadaddlem  13654  isprm3  13764  maxprmfct  13791  pclem  13897  prmreclem1  13969  prmreclem2  13970  prmreclem3  13971  1arith  13980  4sqlem11  14008  ramtlecl  14053  ramcl2lem  14062  ramxrcl  14070  cshwshashlem1  14114  structfn  14179  strlemor1  14257  strleun  14260  srngbase  14286  srngplusg  14287  srngmulr  14288  lmodbase  14295  lmodplusg  14296  lmodsca  14297  ipsbase  14302  ipsaddg  14303  ipsmulr  14304  ipssca  14305  ipsvsca  14306  ipsip  14307  phlbase  14312  phlplusg  14313  phlsca  14314  phlvsca  14315  phlip  14316  odrngbas  14338  odrngplusg  14339  odrngmulr  14340  odrngtset  14341  odrngle  14342  odrngds  14343  prdsval  14385  prdssca  14386  prdsbas  14387  prdsplusg  14388  prdsmulr  14389  prdsvsca  14390  prdsip  14391  prdsle  14392  prdsds  14394  prdstset  14396  prdshom  14397  prdsco  14398  imasbas  14442  imasds  14443  imasplusg  14447  imasmulr  14448  imassca  14449  imasvsca  14450  imasip  14451  imastset  14452  imasle  14453  wunfunc  14801  fullfunc  14808  fthfunc  14809  isfull  14812  isfth  14816  wunnat  14858  dmcoass  14926  catcisolem  14966  catciso  14967  catcoppccl  14968  catcfuccl  14969  catcxpccl  15009  ipobas  15317  ipolerval  15318  ipotset  15319  psdmrn  15369  psss  15376  ledm  15386  lern  15387  dirdm  15396  dirge  15399  mvdco  15942  f1omvdconj  15943  gexex  16326  gsumval3OLD  16373  gsumval3  16376  gsumzaddlemOLD  16401  lssacs  17028  asplss  17380  aspsubrg  17382  psrass1lem  17427  psrbas  17428  psrbasOLD  17429  psrplusg  17432  psrmulr  17435  psrsca  17440  psrvscafval  17441  psrass1  17458  psrdi  17459  psrdir  17460  psrcom  17461  psrass23  17462  psropprmul  17673  coe1mul2  17703  cnfldbas  17802  cnfldadd  17803  cnfldmul  17804  cnfldcj  17805  cnfldtset  17806  cnfldle  17807  cnfldds  17808  cnfldunif  17809  rge0srg  17862  zntoslem  17969  ofco2  18312  leordtval2  18796  lmbrf  18844  lmres  18884  fiuncmp  18987  1stckgenlem  19106  kgencn3  19111  ptbasfi  19134  xkoopn  19142  txcnmpt  19177  txkgen  19205  opnfbas  19395  fmfnfmlem4  19510  tsmsxplem1  19707  trust  19784  restutop  19792  nmoffn  20270  nmofval  20273  nmogelb  20275  nmolb  20276  nmof  20278  qtopbas  20318  tgqioo  20357  re2ndc  20358  iitopon  20435  dfii3  20439  iimulcn  20490  cnheiborlem  20506  bndth  20510  lebnumii  20518  reparphti  20549  pcoass  20576  cphsqrcl  20683  lmmbrf  20753  iscauf  20771  caucfil  20774  lmclimf  20794  rrxmval  20884  rrxmet  20887  ovolfioo  20931  ovolficc  20932  ovolficcss  20933  ovolfsf  20935  ovollb  20942  ovolicc2lem3  20982  ovolicc2lem4  20983  ovolicc2  20985  volf  20992  volsup  21017  ovolfs2  21031  uniiccdif  21038  uniioovol  21039  uniiccvol  21040  uniioombllem2  21043  uniioombllem3a  21044  uniioombllem3  21045  uniioombllem4  21046  uniioombllem5  21047  uniioombl  21049  dyadmbllem  21059  dyadmbl  21060  opnmbllem  21061  opnmblALT  21063  volsup2  21065  vitalilem4  21071  vitalilem5  21072  vitali  21073  mbfimaopnlem  21113  mbflimsup  21124  i1f0  21145  i1f1  21148  itg11  21149  itg2mulc  21205  itg2gt0  21218  ellimc2  21332  limcresi  21340  dvreslem  21364  dvres2lem  21365  dvaddbr  21392  dvmulbr  21393  dvlipcn  21446  c1liplem1  21448  lhop1lem  21465  lhop1  21466  lhop2  21467  lhop  21468  dvfsumrlim  21483  ftc1cn  21495  itgsubstlem  21500  itgsubst  21501  mdegleb  21515  mdeglt  21516  mdegldg  21517  mdegxrcl  21518  mdegcl  21520  mdegaddle  21525  mdegmullem  21529  deg1mul3le  21568  ig1peu  21623  ig1pdvds  21628  aacjcl  21773  aannenlem2  21775  aannenlem3  21776  aalioulem2  21779  taylfval  21804  radcnvcl  21862  radcnvlt1  21863  radcnvle  21865  abelth  21886  abelth2  21887  pilem2  21897  pilem3  21898  pige3  21959  recosf1o  21971  resinf1o  21972  tanord1  21973  logcn  22072  dvlog  22076  dvlog2lem  22077  efopn  22083  logtayl  22085  cxpcn3  22166  loglesqr  22176  ssscongptld  22200  leibpi  22317  efrlim  22343  jensenlem1  22360  jensenlem2  22361  jensen  22362  amgm  22364  ftalem5  22394  efnnfsumcl  22420  efchtdvds  22477  dvdsmulf1o  22514  fsumdvdsmul  22515  lgsfcl2  22621  2sqlem6  22688  2sqlem8  22691  2sqlem9  22692  rpvmasumlem  22716  rpvmasum2  22741  dchrisum0re  22742  dchrisum0lem3  22748  dchrisum0  22749  rplogsum  22756  dirith2  22757  axtgcgrrflx  22903  axtgcgrid  22904  axtgsegcon  22905  axtg5seg  22906  axtgbtwnid  22907  axtgpasch  22908  axtgcont1  22909  tglng  22960  umgrass  23221  constr3pthlem1  23509  nmlno0lem  24161  hlimcaui  24607  chsspwh  24618  shsss  24684  chintcli  24702  shsleji  24741  shub1i  24745  shsval2i  24758  lejdii  24909  spanuni  24915  sshhococi  24917  spansnpji  24949  osumcori  25014  5oai  25032  3oalem6  25038  3oai  25039  pjssmii  25052  mayete3i  25099  mayete3iOLD  25100  mayetes3i  25101  nmlnop0iALT  25367  imaelshi  25430  pjnmopi  25520  pjclem1  25567  pjci  25572  mdslmd1lem1  25697  shatomistici  25733  hatomistici  25734  chpssati  25735  xppreima  25932  iundisjfi  26048  iundisj2fi  26049  xrsmulgzz  26107  fsumrp0cl  26126  gsumunsnf  26213  gsumle  26214  gsummpt2co  26217  xrge0slmod  26281  unitsscn  26295  ordtconlem1  26323  xrge0iifhom  26336  lmlimxrge0  26347  lmxrge0  26351  esumcst  26483  esumpfinvallem  26492  esumpfinval  26493  esumpfinvalf  26494  esumcvg  26504  measunl  26599  imambfm  26646  elmbfmvol2  26651  sxbrsigalem3  26656  sxbrsigalem2  26670  sxbrsigalem4  26671  sitgclg  26697  eulerpartlem1  26719  eulerpartlemgvv  26728  eulerpartlemgh  26730  eulerpartlemgf  26731  ballotlemfc0  26844  ballotlemfcc  26845  ballotlemiex  26853  ballotlemsup  26856  ballotlemsdom  26863  ballotlemsima  26867  ballotlemrv2  26873  ballotth  26889  signsplypnf  26920  signsply0  26921  lgamgulmlem2  26985  subfacp1lem2a  27037  erdszelem4  27051  erdszelem5  27052  erdszelem7  27054  erdszelem8  27055  kur14lem7  27069  kur14lem9  27071  cvxpcon  27100  cvxscon  27101  rescon  27104  iccllyscon  27108  prodmolem2a  27416  prodmolem2  27417  zprod  27419  fprodrpcl  27438  rprisefaccl  27495  txpss3v  27878  txprel  27879  limitssson  27911  onint1  28265  opnmbllem0  28398  mblfinlem1  28399  mblfinlem2  28400  mblfinlem3  28401  mblfinlem4  28402  ismblfin  28403  mbfposadd  28410  cnambfre  28411  itg2addnc  28417  ftc1cnnclem  28436  ftc1cnnc  28437  ftc1anclem3  28440  ftc1anclem7  28444  ftc1anc  28446  ftc2nc  28447  dvreasin  28453  dvreacos  28454  areacirclem1  28455  areacirclem2  28456  areacirc  28460  finminlem  28484  comppfsc  28550  tailf  28567  filnetlem3  28572  caures  28627  reheibor  28709  diophin  29082  4rexfrabdioph  29107  6rexfrabdioph  29108  irrapxlem1  29134  irrapx1  29140  monotuz  29253  jm2.27dlem5  29333  hbtlem2  29451  algbase  29506  algaddg  29507  algmulr  29508  algsca  29509  algvsca  29510  itgpowd  29561  arearect  29562  areaquad  29563  lhe4.4ex1a  29574  itgsin0pilem1  29761  itgsinexplem1  29765  itgsinexp  29766  wallispilem2  29832  disjxwwlkn  30535  psrass23l  30790  relopabVD  31566  bnj1145  31913  bnj1286  31939  bj-unrab  32329  bj-2upln1upl  32417  bj-rrveccmnd  32483  atlatmstc  32857  atlatle  32858  pmaple  33298  sspadd1  33352  sspadd2  33353  taupilem2  35509  taupi  35510
  Copyright terms: Public domain W3C validator