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

Theorem sstri 3409
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 3407 . 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 3372
This theorem was proved from axioms:  ax-mp 5  ax-1 6  ax-2 7  ax-3 8  ax-gen 1663  ax-4 1676  ax-5 1752  ax-6 1798  ax-7 1843  ax-10 1891  ax-11 1896  ax-12 1909  ax-13 2058  ax-ext 2402
This theorem depends on definitions:  df-bi 188  df-an 372  df-tru 1440  df-ex 1658  df-nf 1662  df-sb 1791  df-clab 2409  df-cleq 2415  df-clel 2418  df-in 3379  df-ss 3386
This theorem is referenced by:  snsstp1  4087  snsstp2  4088  uniintsn  4229  ssrnres  5230  cossxp  5313  foimacnv  5784  ssimaex  5883  riotassuni  6240  oprabss  6333  dmexg  6675  rnexg  6676  fabexg  6700  fparlem3  6846  fparlem4  6847  snopsuppss  6877  tposssxp  6925  mapsspw  7455  sbthlem5  7632  sbthlem7  7634  cnvimamptfin  7821  marypha1lem  7893  ordtypelem4  7982  hartogslem1  8003  tc2  8171  tz9.12lem1  8203  rankval4  8283  rankxpl  8291  rankmapu  8294  rankxplim  8295  infxpenlem  8389  ackbij1lem18  8611  cflm  8624  fin23lem29  8715  hsmexlem4  8803  hsmexlem5  8804  brdom3  8900  brdom5  8901  brdom4  8902  smobeth  8955  pwfseqlem3  9029  wundm  9097  wunrn  9098  wunex2  9107  ltsopi  9257  dmaddpi  9259  dmmulpi  9260  nqerf  9299  ltrelxr  9639  nnsscn  10558  nn0sscn  10818  uzwo2  11167  uzinfmiOLD  11183  infssuzle  11188  infssuzcl  11189  infmssuzleOLD  11190  infmssuzclOLD  11191  uzwo3  11203  nn0ssq  11216  nnssq  11217  qsscn  11219  rpnnen1lem3  11236  rpnnen1lem5  11238  dflt2  11391  fzval2  11731  fzof  11861  fzossnn  11907  fzo0ssnn0  11937  injresinj  11968  flval3  11993  uzsup  12033  uzrdgfni  12115  expcl2lem  12227  rpexpcl  12234  expge0  12251  expge1  12252  hashxrcl  12482  seqcoll  12568  wrdexg  12623  xptrrel  12981  trclublem  12996  sqrlem3  13245  limsupval2  13476  limsupval2OLD  13477  limsupgre  13478  limsupgreOLD  13479  rlimpm  13500  rlimclim  13546  isercolllem1  13664  isercolllem2  13665  isercoll  13667  caurcvg  13678  caurcvgOLD  13679  caucvg  13681  summolem2a  13717  summolem2  13718  zsum  13720  fsumcvg3  13731  fsumrpcl  13739  fsumge0  13791  climfsum  13816  ackbijnn  13822  prodmolem2a  13924  prodmolem2  13925  zprod  13927  fprodrpcl  13946  fprodge0  13983  fprodge1  13985  rprisefaccl  14012  divalglem8  14316  sadaddlem  14376  lcmfval  14527  lcmfvalOLD  14531  isprm3  14569  maxprmfct  14588  pclem  14724  prmreclem1  14796  prmreclem2  14797  prmreclem3  14798  1arith  14807  4sqlem11  14835  ramtlecl  14887  ramcl2lem  14898  ramcl2lemOLD  14899  ramxrcl  14911  prmgaplem3  14959  prmgaplem4  14960  cshwshashlem1  15002  structfn  15070  strlemor1  15153  strleun  15156  srngbase  15189  srngplusg  15190  srngmulr  15191  lmodbase  15198  lmodplusg  15199  lmodsca  15200  ipsbase  15205  ipsaddg  15206  ipsmulr  15207  ipssca  15208  ipsvsca  15209  ipsip  15210  phlbase  15215  phlplusg  15216  phlsca  15217  phlvsca  15218  phlip  15219  odrngbas  15241  odrngplusg  15242  odrngmulr  15243  odrngtset  15244  odrngle  15245  odrngds  15246  prdsval  15289  prdssca  15290  prdsbas  15291  prdsplusg  15292  prdsmulr  15293  prdsvsca  15294  prdsip  15295  prdsle  15296  prdsds  15298  prdstset  15300  prdshom  15301  prdsco  15302  imasbas  15349  imasds  15350  imasplusg  15354  imasmulr  15355  imassca  15356  imasvsca  15357  imasip  15358  imastset  15359  imasle  15360  imasbasOLD  15361  imasdsOLD  15362  wunfunc  15740  fullfunc  15747  fthfunc  15748  isfull  15751  isfth  15755  wunnat  15797  dmcoass  15897  catcisolem  15937  catciso  15938  catcoppccl  15939  catcfuccl  15940  catcxpccl  16028  ipobas  16337  ipolerval  16338  ipotset  16339  psdmrn  16389  psss  16396  ledm  16406  lern  16407  dirdm  16416  dirge  16419  mvdco  17022  f1omvdconj  17023  gexex  17427  gsumval3  17477  lssacs  18126  asplss  18489  aspsubrg  18491  psrass1lem  18537  psrbas  18538  psrplusg  18541  psrmulr  18544  psrsca  18549  psrvscafval  18550  psrass1  18565  psrass23l  18568  psrcom  18569  psrass23  18570  psropprmul  18767  coe1mul2  18798  cnfldbas  18910  cnfldadd  18911  cnfldmul  18912  cnfldcj  18913  cnfldtset  18914  cnfldle  18915  cnfldds  18916  cnfldunif  18917  rge0srg  18973  zntoslem  19062  ofco2  19411  leordtval2  20163  lmbrf  20211  lmres  20251  fiuncmp  20354  comppfsc  20482  1stckgenlem  20503  kgencn3  20508  ptbasfi  20531  xkoopn  20539  txcnmpt  20574  txkgen  20602  opnfbas  20792  fmfnfmlem4  20907  tsmsxplem1  21102  trust  21179  restutop  21187  nmoffn  21651  nmofval  21654  nmogelb  21656  nmolb  21657  nmof  21659  nmoffnOLD  21672  nmofvalOLD  21673  nmogelbOLD  21675  nmolbOLD  21676  nmofOLD  21677  qtopbas  21715  tgqioo  21753  re2ndc  21754  iitopon  21846  dfii3  21850  iimulcn  21901  cnheiborlem  21917  bndth  21921  lebnumii  21932  reparphti  21963  pcoass  21990  cphsqrtcl  22097  lmmbrf  22167  iscauf  22185  caucfil  22188  lmclimf  22208  rrxmval  22294  rrxmet  22297  ovolfioo  22355  ovolficc  22356  ovolficcss  22357  ovolfsf  22359  ovollb  22367  ovolicc2lem3  22407  ovolicc2lem4OLD  22408  ovolicc2lem4  22409  ovolicc2  22411  volf  22418  volsup  22444  ovolfs2  22458  uniiccdif  22470  uniioovol  22471  uniiccvol  22472  uniioombllem2  22475  uniioombllem2OLD  22476  uniioombllem3a  22477  uniioombllem3  22478  uniioombllem4  22479  uniioombllem5  22480  uniioombl  22482  dyadmbllem  22492  dyadmbl  22493  opnmbllem  22494  opnmblALT  22496  volsup2  22498  vitalilem4  22504  vitalilem5  22505  vitali  22506  mbfimaopnlem  22546  mbflimsup  22558  mbflimsupOLD  22559  i1f0  22580  i1f1  22583  itg11  22584  itg2mulc  22640  itg2gt0  22653  ellimc2  22767  limcresi  22775  dvreslem  22799  dvres2lem  22800  dvaddbr  22827  dvmulbr  22828  dvlipcn  22881  c1liplem1  22883  lhop1lem  22900  lhop1  22901  lhop2  22902  lhop  22903  dvfsumrlim  22918  ftc1cn  22930  itgsubstlem  22935  itgsubst  22936  mdegleb  22948  mdeglt  22949  mdegldg  22950  mdegxrcl  22951  mdegcl  22953  mdegaddle  22958  mdegmullem  22962  deg1mul3le  23000  ig1peu  23057  ig1peuOLD  23058  ig1pdvds  23063  ig1pdvdsOLD  23069  aacjcl  23218  aannenlem2  23220  aannenlem3  23221  aalioulem2  23224  taylfval  23249  radcnvcl  23307  radcnvlt1  23308  radcnvle  23310  abelth  23331  abelth2  23332  pilem2  23342  pilem2OLD  23343  pilem3  23344  pilem3OLD  23345  pige3  23407  recosf1o  23419  resinf1o  23420  tanord1  23421  logcn  23527  dvlog  23531  dvlog2lem  23532  efopn  23538  logtayl  23540  cxpcn3  23623  loglesqrt  23633  ssscongptld  23686  leibpi  23803  efrlim  23830  jensenlem1  23847  jensenlem2  23848  jensen  23849  amgm  23851  lgamgulmlem2  23890  ftalem5  23936  ftalem5OLD  23938  efnnfsumcl  23964  efchtdvds  24021  dvdsmulf1o  24058  fsumdvdsmul  24059  lgsfcl2  24165  2sqlem6  24232  2sqlem8  24235  2sqlem9  24236  rpvmasumlem  24260  rpvmasum2  24285  dchrisum0re  24286  dchrisum0lem3  24292  dchrisum0  24293  rplogsum  24300  dirith2  24301  axtgcgrrflx  24445  axtgcgrid  24446  axtgsegcon  24447  axtg5seg  24448  axtgbtwnid  24449  axtgpasch  24450  axtgcont1  24451  tgcgr4  24511  motcgrg  24524  tglng  24526  umgrass  24981  constr3pthlem1  25318  disjxwwlkn  25408  nmlno0lem  26369  hlimcaui  26824  chsspwh  26835  shsss  26901  chintcli  26919  shsleji  26958  shub1i  26962  shsval2i  26975  lejdii  27126  spanuni  27132  sshhococi  27134  spansnpji  27166  osumcori  27231  5oai  27249  3oalem6  27255  3oai  27256  pjssmii  27269  mayete3i  27316  mayetes3i  27317  nmlnop0iALT  27583  imaelshi  27646  pjnmopi  27736  pjclem1  27783  pjci  27788  mdslmd1lem1  27913  shatomistici  27949  hatomistici  27950  chpssati  27951  xppreima  28187  iundisjfi  28315  iundisj2fi  28316  xrsmulgzz  28384  fsumrp0cl  28402  gsummpt2co  28487  xrge0slmod  28552  unitsscn  28647  ordtconlem1  28675  xrge0iifhom  28688  lmlimxrge0  28699  lmxrge0  28703  esumcst  28829  esumpfinvallem  28840  esumpfinval  28841  esumpfinvalf  28842  esumcvg  28852  imambfm  29029  elmbfmvol2  29034  sxbrsigalem3  29039  sxbrsigalem2  29053  sxbrsigalem4  29054  sitgclg  29120  eulerpartlem1  29145  eulerpartlemgvv  29154  eulerpartlemgh  29156  eulerpartlemgf  29157  ballotlemfc0  29270  ballotlemfcc  29271  ballotlemiex  29279  ballotlemsup  29282  ballotlemsdom  29289  ballotlemsima  29293  ballotlemrv2  29299  ballotth  29315  ballotlemiexOLD  29317  ballotlemsupOLD  29320  ballotlemsdomOLD  29327  ballotlemsimaOLD  29331  ballotlemrv2OLD  29337  ballotthOLD  29353  signsplypnf  29384  signsply0  29385  bnj1145  29747  bnj1286  29773  subfacp1lem2a  29848  erdszelem4  29862  erdszelem5  29863  erdszelem7  29865  erdszelem8  29866  kur14lem7  29880  kur14lem9  29882  cvxpcon  29910  cvxscon  29911  rescon  29914  iccllyscon  29918  txpss3v  30587  txprel  30588  limitssson  30620  finminlem  30916  tailf  30973  filnetlem3  30978  onint1  31051  bj-unrab  31435  bj-2upln1upl  31523  bj-rrvecsscmn  31608  taupilem2  31624  taupi  31625  poimirlem3  31844  poimirlem30  31871  poimirlem31  31872  poimirlem32  31873  broucube  31875  opnmbllem0  31877  mblfinlem1  31878  mblfinlem2  31879  mblfinlem3  31880  mblfinlem4  31881  ismblfin  31882  mbfposadd  31889  cnambfre  31890  itg2addnc  31897  ftc1cnnclem  31916  ftc1cnnc  31917  ftc1anclem3  31920  ftc1anclem7  31924  ftc1anc  31926  ftc2nc  31927  dvreasin  31931  dvreacos  31932  areacirclem1  31933  areacirclem2  31934  areacirc  31938  caures  31990  reheibor  32072  atlatmstc  32791  atlatle  32792  pmaple  33232  sspadd1  33286  sspadd2  33287  diophin  35521  4rexfrabdioph  35547  6rexfrabdioph  35548  irrapxlem1  35573  irrapx1  35579  monotuz  35696  jm2.27dlem5  35775  hbtlem2  35890  algbase  35951  algaddg  35952  algmulr  35953  algsca  35954  algvsca  35955  itgpowd  36006  arearect  36007  areaquad  36008  rtrclex  36131  trclubgNEW  36132  trclexi  36134  rtrclexi  36135  cnvtrcl0  36140  dfrtrcl5  36143  trrelsuperrel2dg  36170  relexpaddss  36217  brtrclfv2  36226  frege131d  36263  xphe  36283  idhe  36290  lhe4.4ex1a  36585  uzmptshftfval  36602  binomcxplemdvbinom  36609  binomcxplemcvg  36610  binomcxplemnotnn0  36612  relopabVD  37208  fzisoeu  37409  fzsscn  37422  fzssre  37426  ioosscn  37477  limcresiooub  37600  limcresioolb  37601  limcleqr  37602  limclner  37609  limclr  37613  icccncfext  37642  cncficcgt0  37643  ioodvbdlimc1lem2  37681  ioodvbdlimc1lem2OLD  37683  ioodvbdlimc2lem  37685  ioodvbdlimc2lemOLD  37686  dvnprodlem1  37698  dvnprodlem2  37699  itgsin0pilem1  37703  itgsinexplem1  37707  itgsinexp  37708  dirkercncflem2  37843  fourierdlem16  37862  fourierdlem18  37864  fourierdlem20  37866  fourierdlem21  37867  fourierdlem22  37868  fourierdlem25  37871  fourierdlem37  37884  fourierdlem42  37889  fourierdlem42OLD  37890  fourierdlem50  37897  fourierdlem52  37899  fourierdlem62  37909  fourierdlem64  37911  fourierdlem66  37913  fourierdlem68  37915  fourierdlem74  37921  fourierdlem75  37922  fourierdlem76  37923  fourierdlem79  37926  fourierdlem83  37930  fourierdlem95  37942  fourierdlem101  37948  fourierdlem102  37949  fourierdlem103  37950  fourierdlem104  37951  fourierdlem112  37959  fourierdlem114  37961  sqwvfoura  37969  sqwvfourb  37970  fouriersw  37972  etransclem24  38000  etransclem48OLD  38024  etransclem48  38025  sge0sn  38066  sge0tsms  38067  sge0f1o  38069  sge0pr  38081  sge0resplit  38093  sge0split  38096  sge0iunmptlemre  38102  sge0isummpt2  38119  carageniuncllem1  38187  hoicvr  38211  hoicvrrex  38219  hoidmvlelem2  38259  upgrss  38948  oddibas  39398  2zrngbas  39521  2zrng0  39523  aacllem  40127
  Copyright terms: Public domain W3C validator