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

Theorem sstri 3353
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 3351 . 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 3316
This theorem was proved from axioms:  ax-mp 5  ax-1 6  ax-2 7  ax-3 8  ax-gen 1594  ax-4 1605  ax-5 1669  ax-6 1707  ax-7 1727  ax-10 1774  ax-11 1779  ax-12 1791  ax-13 1942  ax-ext 2414
This theorem depends on definitions:  df-bi 185  df-an 371  df-ex 1590  df-nf 1593  df-sb 1700  df-clab 2420  df-cleq 2426  df-clel 2429  df-in 3323  df-ss 3330
This theorem is referenced by:  snsstp1  4012  snsstp2  4013  uniintsn  4153  ssrnres  5264  cossxp  5348  foimacnv  5646  ssimaex  5744  riotassuniOLD  6078  oprabss  6165  dmexg  6498  rnexg  6499  fabexg  6522  fparlem3  6663  fparlem4  6664  snopsuppss  6694  tposssxp  6738  mapsspw  7236  sbthlem5  7413  sbthlem7  7415  cnvimamptfin  7600  marypha1lem  7671  ordtypelem4  7723  hartogslem1  7744  tc2  7950  tz9.12lem1  7982  rankval4  8062  rankxpl  8070  rankmapu  8073  rankxplim  8074  infxpenlem  8168  ackbij1lem18  8394  cflm  8407  fin23lem29  8498  hsmexlem4  8586  hsmexlem5  8587  brdom3  8683  brdom5  8684  brdom4  8685  smobeth  8738  pwfseqlem3  8814  wundm  8882  wunrn  8883  wunex2  8892  ltsopi  9044  dmaddpi  9046  dmmulpi  9047  nqerf  9086  ltrelxr  9425  nnsscn  10314  nn0sscn  10571  uzwo2  10906  uzinfmi  10921  infmssuzle  10924  infmssuzcl  10925  uzwo3  10935  nn0ssq  10948  nnssq  10949  qsscn  10951  rpnnen1lem3  10968  rpnnen1lem5  10970  dflt2  11112  fzval2  11426  fzof  11533  fzossnn  11577  fzo0ssnn0  11594  injresinj  11622  flval3  11646  uzsup  11685  uzrdgfni  11764  expcl2lem  11860  rpexpcl  11867  expge0  11883  expge1  11884  hashxrcl  12110  seqcoll  12199  wrdexg  12227  seqshft  12557  sqrlem3  12717  limsupval2  12941  limsupgre  12942  rlimpm  12961  rlimclim  13007  isercolllem1  13125  isercolllem2  13126  isercoll  13128  caurcvg  13137  caucvg  13139  summolem2a  13175  summolem2  13176  zsum  13178  fsumcvg3  13189  fsumrpcl  13197  fsumge0  13240  climfsum  13265  ackbijnn  13273  divalglem8  13586  sadaddlem  13644  isprm3  13754  maxprmfct  13781  pclem  13887  prmreclem1  13959  prmreclem2  13960  prmreclem3  13961  1arith  13970  4sqlem11  13998  ramtlecl  14043  ramcl2lem  14052  ramxrcl  14060  cshwshashlem1  14104  structfn  14169  strlemor1  14247  strleun  14250  srngbase  14276  srngplusg  14277  srngmulr  14278  lmodbase  14285  lmodplusg  14286  lmodsca  14287  ipsbase  14292  ipsaddg  14293  ipsmulr  14294  ipssca  14295  ipsvsca  14296  ipsip  14297  phlbase  14302  phlplusg  14303  phlsca  14304  phlvsca  14305  phlip  14306  odrngbas  14328  odrngplusg  14329  odrngmulr  14330  odrngtset  14331  odrngle  14332  odrngds  14333  prdsval  14375  prdssca  14376  prdsbas  14377  prdsplusg  14378  prdsmulr  14379  prdsvsca  14380  prdsip  14381  prdsle  14382  prdsds  14384  prdstset  14386  prdshom  14387  prdsco  14388  imasbas  14432  imasds  14433  imasplusg  14437  imasmulr  14438  imassca  14439  imasvsca  14440  imasip  14441  imastset  14442  imasle  14443  wunfunc  14791  fullfunc  14798  fthfunc  14799  isfull  14802  isfth  14806  wunnat  14848  dmcoass  14916  catcisolem  14956  catciso  14957  catcoppccl  14958  catcfuccl  14959  catcxpccl  14999  ipobas  15307  ipolerval  15308  ipotset  15309  psdmrn  15359  psss  15366  ledm  15376  lern  15377  dirdm  15386  dirge  15389  mvdco  15930  f1omvdconj  15931  gexex  16314  gsumval3OLD  16361  gsumval3  16364  gsumzaddlemOLD  16389  lssacs  16969  asplss  17321  aspsubrg  17323  psrass1lem  17380  psrbas  17381  psrbasOLD  17382  psrplusg  17385  psrmulr  17388  psrsca  17393  psrvscafval  17394  psrass1  17411  psrdi  17412  psrdir  17413  psrcom  17414  psrass23  17415  psropprmul  17590  coe1mul2  17620  cnfldbas  17665  cnfldadd  17666  cnfldmul  17667  cnfldcj  17668  cnfldtset  17669  cnfldle  17670  cnfldds  17671  cnfldunif  17672  zntoslem  17830  ofco2  18173  leordtval2  18657  lmbrf  18705  lmres  18745  fiuncmp  18848  1stckgenlem  18967  kgencn3  18972  ptbasfi  18995  xkoopn  19003  txcnmpt  19038  txkgen  19066  opnfbas  19256  fmfnfmlem4  19371  tsmsxplem1  19568  trust  19645  restutop  19653  nmoffn  20131  nmofval  20134  nmogelb  20136  nmolb  20137  nmof  20139  qtopbas  20179  tgqioo  20218  re2ndc  20219  iitopon  20296  dfii3  20300  iimulcn  20351  cnheiborlem  20367  bndth  20371  lebnumii  20379  reparphti  20410  pcoass  20437  cphsqrcl  20544  lmmbrf  20614  iscauf  20632  caucfil  20635  lmclimf  20655  rrxmval  20745  rrxmet  20748  ovolfioo  20792  ovolficc  20793  ovolficcss  20794  ovolfsf  20796  ovollb  20803  ovolicc2lem3  20843  ovolicc2lem4  20844  ovolicc2  20846  volf  20853  volsup  20878  ovolfs2  20892  uniiccdif  20899  uniioovol  20900  uniiccvol  20901  uniioombllem2  20904  uniioombllem3a  20905  uniioombllem3  20906  uniioombllem4  20907  uniioombllem5  20908  uniioombl  20910  dyadmbllem  20920  dyadmbl  20921  opnmbllem  20922  opnmblALT  20924  volsup2  20926  vitalilem4  20932  vitalilem5  20933  vitali  20934  mbfimaopnlem  20974  mbflimsup  20985  i1f0  21006  i1f1  21009  itg11  21010  itg2mulc  21066  itg2gt0  21079  ellimc2  21193  limcresi  21201  dvreslem  21225  dvres2lem  21226  dvaddbr  21253  dvmulbr  21254  dvlipcn  21307  c1liplem1  21309  lhop1lem  21326  lhop1  21327  lhop2  21328  lhop  21329  dvfsumrlim  21344  ftc1cn  21356  itgsubstlem  21361  itgsubst  21362  mdegleb  21419  mdeglt  21420  mdegldg  21421  mdegxrcl  21422  mdegcl  21424  mdegaddle  21429  mdegmullem  21433  deg1mul3le  21472  ig1peu  21527  ig1pdvds  21532  aacjcl  21677  aannenlem2  21679  aannenlem3  21680  aalioulem2  21683  taylfval  21708  radcnvcl  21766  radcnvlt1  21767  radcnvle  21769  abelth  21790  abelth2  21791  pilem2  21801  pilem3  21802  pige3  21863  recosf1o  21875  resinf1o  21876  tanord1  21877  logcn  21976  dvlog  21980  dvlog2lem  21981  efopn  21987  logtayl  21989  cxpcn3  22070  loglesqr  22080  ssscongptld  22104  leibpi  22221  efrlim  22247  jensenlem1  22264  jensenlem2  22265  jensen  22266  amgm  22268  ftalem5  22298  efnnfsumcl  22324  efchtdvds  22381  dvdsmulf1o  22418  fsumdvdsmul  22419  lgsfcl2  22525  2sqlem6  22592  2sqlem8  22595  2sqlem9  22596  rpvmasumlem  22620  rpvmasum2  22645  dchrisum0re  22646  dchrisum0lem3  22652  dchrisum0  22653  rplogsum  22660  dirith2  22661  axtgcgrrflx  22807  axtgcgrid  22808  axtgsegcon  22809  axtg5seg  22810  axtgbtwnid  22811  axtgpasch  22812  axtgcont1  22813  tglng  22860  umgrass  23075  constr3pthlem1  23363  nmlno0lem  24015  hlimcaui  24461  chsspwh  24472  shsss  24538  chintcli  24556  shsleji  24595  shub1i  24599  shsval2i  24612  lejdii  24763  spanuni  24769  sshhococi  24771  spansnpji  24803  osumcori  24868  5oai  24886  3oalem6  24892  3oai  24893  pjssmii  24906  mayete3i  24953  mayete3iOLD  24954  mayetes3i  24955  nmlnop0iALT  25221  imaelshi  25284  pjnmopi  25374  pjclem1  25421  pjci  25426  mdslmd1lem1  25551  shatomistici  25587  hatomistici  25588  chpssati  25589  xppreima  25787  iundisjfi  25902  iundisj2fi  25903  xrsmulgzz  25961  fsumrp0cl  25981  rge0srg  26063  gsumunsnf  26096  gsumle  26097  gsummpt2co  26100  xrge0slmod  26165  unitsscn  26179  ordtconlem1  26207  xrge0iifhom  26220  lmlimxrge0  26231  lmxrge0  26235  esumcst  26367  esumpfinvallem  26376  esumpfinval  26377  esumpfinvalf  26378  esumcvg  26388  measunl  26483  imambfm  26530  elmbfmvol2  26535  sxbrsigalem3  26540  sxbrsigalem2  26554  sxbrsigalem4  26555  sitgclg  26575  eulerpartlem1  26597  eulerpartlemgvv  26606  eulerpartlemgh  26608  eulerpartlemgf  26609  ballotlemfc0  26722  ballotlemfcc  26723  ballotlemiex  26731  ballotlemsup  26734  ballotlemsdom  26741  ballotlemsima  26745  ballotlemrv2  26751  ballotth  26767  signsplypnf  26798  signsply0  26799  lgamgulmlem2  26863  subfacp1lem2a  26915  erdszelem4  26929  erdszelem5  26930  erdszelem7  26932  erdszelem8  26933  kur14lem7  26947  kur14lem9  26949  cvxpcon  26978  cvxscon  26979  rescon  26982  iccllyscon  26986  prodmolem2a  27293  prodmolem2  27294  zprod  27296  fprodrpcl  27315  rprisefaccl  27372  txpss3v  27755  txprel  27756  limitssson  27788  onint1  28142  opnmbllem0  28268  mblfinlem1  28269  mblfinlem2  28270  mblfinlem3  28271  mblfinlem4  28272  ismblfin  28273  mbfposadd  28280  cnambfre  28281  itg2addnc  28287  ftc1cnnclem  28306  ftc1cnnc  28307  ftc1anclem3  28310  ftc1anclem7  28314  ftc1anc  28316  ftc2nc  28317  dvreasin  28323  dvreacos  28324  areacirclem1  28325  areacirclem2  28326  areacirc  28330  finminlem  28354  comppfsc  28420  tailf  28437  filnetlem3  28442  caures  28497  reheibor  28579  diophin  28953  4rexfrabdioph  28978  6rexfrabdioph  28979  irrapxlem1  29005  irrapx1  29011  monotuz  29124  jm2.27dlem5  29204  hbtlem2  29322  algbase  29377  algaddg  29378  algmulr  29379  algsca  29380  algvsca  29381  itgpowd  29432  arearect  29433  areaquad  29434  lhe4.4ex1a  29445  itgsin0pilem1  29633  itgsinexplem1  29637  itgsinexp  29638  wallispilem2  29704  disjxwwlkn  30407  relopabVD  31336  bnj1145  31683  bnj1286  31709  bj-unrab  32012  bj-2upln1upl  32097  bj-rrveccmnd  32160  atlatmstc  32534  atlatle  32535  pmaple  32975  sspadd1  33029  sspadd2  33030  taupilem2  35186  taupi  35187
  Copyright terms: Public domain W3C validator