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

Theorem sstri 3498
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 3496 . 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 3461
This theorem was proved from axioms:  ax-mp 5  ax-1 6  ax-2 7  ax-3 8  ax-gen 1623  ax-4 1636  ax-5 1709  ax-6 1752  ax-7 1795  ax-10 1842  ax-11 1847  ax-12 1859  ax-13 2004  ax-ext 2432
This theorem depends on definitions:  df-bi 185  df-an 369  df-tru 1401  df-ex 1618  df-nf 1622  df-sb 1745  df-clab 2440  df-cleq 2446  df-clel 2449  df-in 3468  df-ss 3475
This theorem is referenced by:  snsstp1  4167  snsstp2  4168  uniintsn  4309  ssrnres  5430  cossxp  5513  foimacnv  5815  ssimaex  5913  riotassuniOLD  6268  oprabss  6361  dmexg  6704  rnexg  6705  fabexg  6729  fparlem3  6875  fparlem4  6876  snopsuppss  6906  tposssxp  6951  mapsspw  7447  sbthlem5  7624  sbthlem7  7626  cnvimamptfin  7813  marypha1lem  7885  ordtypelem4  7938  hartogslem1  7959  tc2  8164  tz9.12lem1  8196  rankval4  8276  rankxpl  8284  rankmapu  8287  rankxplim  8288  infxpenlem  8382  ackbij1lem18  8608  cflm  8621  fin23lem29  8712  hsmexlem4  8800  hsmexlem5  8801  brdom3  8897  brdom5  8898  brdom4  8899  smobeth  8952  pwfseqlem3  9027  wundm  9095  wunrn  9096  wunex2  9105  ltsopi  9255  dmaddpi  9257  dmmulpi  9258  nqerf  9297  ltrelxr  9637  nnsscn  10536  nn0sscn  10796  uzwo2  11147  uzinfmi  11162  infmssuzle  11165  infmssuzcl  11166  uzwo3  11178  nn0ssq  11191  nnssq  11192  qsscn  11194  rpnnen1lem3  11211  rpnnen1lem5  11213  dflt2  11357  fzval2  11678  fzof  11801  fzossnn  11847  fzo0ssnn0  11877  injresinj  11907  flval3  11932  uzsup  11972  uzrdgfni  12051  expcl2lem  12160  rpexpcl  12167  expge0  12184  expge1  12185  hashxrcl  12411  seqcoll  12496  wrdexg  12544  xptrrel  12898  trclublem  12913  sqrlem3  13160  limsupval2  13385  limsupgre  13386  rlimpm  13405  rlimclim  13451  isercolllem1  13569  isercolllem2  13570  isercoll  13572  caurcvg  13581  caucvg  13583  summolem2a  13619  summolem2  13620  zsum  13622  fsumcvg3  13633  fsumrpcl  13641  fsumge0  13691  climfsum  13716  ackbijnn  13722  prodmolem2a  13823  prodmolem2  13824  zprod  13826  fprodrpcl  13845  divalglem8  14142  sadaddlem  14200  isprm3  14310  maxprmfct  14338  pclem  14446  prmreclem1  14518  prmreclem2  14519  prmreclem3  14520  1arith  14529  4sqlem11  14557  ramtlecl  14602  ramcl2lem  14611  ramxrcl  14619  cshwshashlem1  14664  structfn  14729  strlemor1  14811  strleun  14814  srngbase  14844  srngplusg  14845  srngmulr  14846  lmodbase  14853  lmodplusg  14854  lmodsca  14855  ipsbase  14860  ipsaddg  14861  ipsmulr  14862  ipssca  14863  ipsvsca  14864  ipsip  14865  phlbase  14870  phlplusg  14871  phlsca  14872  phlvsca  14873  phlip  14874  odrngbas  14896  odrngplusg  14897  odrngmulr  14898  odrngtset  14899  odrngle  14900  odrngds  14901  prdsval  14944  prdssca  14945  prdsbas  14946  prdsplusg  14947  prdsmulr  14948  prdsvsca  14949  prdsip  14950  prdsle  14951  prdsds  14953  prdstset  14955  prdshom  14956  prdsco  14957  imasbas  15001  imasds  15002  imasplusg  15006  imasmulr  15007  imassca  15008  imasvsca  15009  imasip  15010  imastset  15011  imasle  15012  wunfunc  15387  fullfunc  15394  fthfunc  15395  isfull  15398  isfth  15402  wunnat  15444  dmcoass  15544  catcisolem  15584  catciso  15585  catcoppccl  15586  catcfuccl  15587  catcxpccl  15675  ipobas  15984  ipolerval  15985  ipotset  15986  psdmrn  16036  psss  16043  ledm  16053  lern  16054  dirdm  16063  dirge  16066  mvdco  16669  f1omvdconj  16670  gexex  17058  gsumval3OLD  17107  gsumval3  17110  gsumzaddlemOLD  17135  lssacs  17808  asplss  18173  aspsubrg  18175  psrass1lem  18224  psrbas  18225  psrbasOLD  18226  psrplusg  18229  psrmulr  18232  psrsca  18237  psrvscafval  18238  psrass1  18255  psrass23l  18258  psrcom  18259  psrass23  18260  psropprmul  18474  coe1mul2  18505  cnfldbas  18619  cnfldadd  18620  cnfldmul  18621  cnfldcj  18622  cnfldtset  18623  cnfldle  18624  cnfldds  18625  cnfldunif  18626  rge0srg  18682  zntoslem  18768  ofco2  19120  leordtval2  19880  lmbrf  19928  lmres  19968  fiuncmp  20071  comppfsc  20199  1stckgenlem  20220  kgencn3  20225  ptbasfi  20248  xkoopn  20256  txcnmpt  20291  txkgen  20319  opnfbas  20509  fmfnfmlem4  20624  tsmsxplem1  20821  trust  20898  restutop  20906  nmoffn  21384  nmofval  21387  nmogelb  21389  nmolb  21390  nmof  21392  qtopbas  21432  tgqioo  21471  re2ndc  21472  iitopon  21549  dfii3  21553  iimulcn  21604  cnheiborlem  21620  bndth  21624  lebnumii  21632  reparphti  21663  pcoass  21690  cphsqrtcl  21797  lmmbrf  21867  iscauf  21885  caucfil  21888  lmclimf  21908  rrxmval  21998  rrxmet  22001  ovolfioo  22045  ovolficc  22046  ovolficcss  22047  ovolfsf  22049  ovollb  22056  ovolicc2lem3  22096  ovolicc2lem4  22097  ovolicc2  22099  volf  22106  volsup  22132  ovolfs2  22146  uniiccdif  22153  uniioovol  22154  uniiccvol  22155  uniioombllem2  22158  uniioombllem3a  22159  uniioombllem3  22160  uniioombllem4  22161  uniioombllem5  22162  uniioombl  22164  dyadmbllem  22174  dyadmbl  22175  opnmbllem  22176  opnmblALT  22178  volsup2  22180  vitalilem4  22186  vitalilem5  22187  vitali  22188  mbfimaopnlem  22228  mbflimsup  22239  i1f0  22260  i1f1  22263  itg11  22264  itg2mulc  22320  itg2gt0  22333  ellimc2  22447  limcresi  22455  dvreslem  22479  dvres2lem  22480  dvaddbr  22507  dvmulbr  22508  dvlipcn  22561  c1liplem1  22563  lhop1lem  22580  lhop1  22581  lhop2  22582  lhop  22583  dvfsumrlim  22598  ftc1cn  22610  itgsubstlem  22615  itgsubst  22616  mdegleb  22630  mdeglt  22631  mdegldg  22632  mdegxrcl  22633  mdegcl  22635  mdegaddle  22640  mdegmullem  22644  deg1mul3le  22683  ig1peu  22738  ig1pdvds  22743  aacjcl  22889  aannenlem2  22891  aannenlem3  22892  aalioulem2  22895  taylfval  22920  radcnvcl  22978  radcnvlt1  22979  radcnvle  22981  abelth  23002  abelth2  23003  pilem2  23013  pilem3  23014  pige3  23076  recosf1o  23088  resinf1o  23089  tanord1  23090  logcn  23196  dvlog  23200  dvlog2lem  23201  efopn  23207  logtayl  23209  cxpcn3  23290  loglesqrt  23300  ssscongptld  23353  leibpi  23470  efrlim  23497  jensenlem1  23514  jensenlem2  23515  jensen  23516  amgm  23518  ftalem5  23548  efnnfsumcl  23574  efchtdvds  23631  dvdsmulf1o  23668  fsumdvdsmul  23669  lgsfcl2  23775  2sqlem6  23842  2sqlem8  23845  2sqlem9  23846  rpvmasumlem  23870  rpvmasum2  23895  dchrisum0re  23896  dchrisum0lem3  23902  dchrisum0  23903  rplogsum  23910  dirith2  23911  axtgcgrrflx  24057  axtgcgrid  24058  axtgsegcon  24059  axtg5seg  24060  axtgbtwnid  24061  axtgpasch  24062  axtgcont1  24063  motcgrg  24132  tglng  24134  umgrass  24521  constr3pthlem1  24857  disjxwwlkn  24947  nmlno0lem  25906  hlimcaui  26352  chsspwh  26363  shsss  26429  chintcli  26447  shsleji  26486  shub1i  26490  shsval2i  26503  lejdii  26654  spanuni  26660  sshhococi  26662  spansnpji  26694  osumcori  26759  5oai  26777  3oalem6  26783  3oai  26784  pjssmii  26797  mayete3i  26844  mayete3iOLD  26845  mayetes3i  26846  nmlnop0iALT  27112  imaelshi  27175  pjnmopi  27265  pjclem1  27312  pjci  27317  mdslmd1lem1  27442  shatomistici  27478  hatomistici  27479  chpssati  27480  xppreima  27708  iundisjfi  27835  iundisj2fi  27836  xrsmulgzz  27900  fsumrp0cl  27919  gsummpt2co  28005  xrge0slmod  28069  unitsscn  28113  ordtconlem1  28141  xrge0iifhom  28154  lmlimxrge0  28165  lmxrge0  28169  esumcst  28292  esumpfinvallem  28303  esumpfinval  28304  esumpfinvalf  28305  esumcvg  28315  imambfm  28470  elmbfmvol2  28475  sxbrsigalem3  28480  sxbrsigalem2  28494  sxbrsigalem4  28495  sitgclg  28548  eulerpartlem1  28570  eulerpartlemgvv  28579  eulerpartlemgh  28581  eulerpartlemgf  28582  ballotlemfc0  28695  ballotlemfcc  28696  ballotlemiex  28704  ballotlemsup  28707  ballotlemsdom  28714  ballotlemsima  28718  ballotlemrv2  28724  ballotth  28740  signsplypnf  28771  signsply0  28772  lgamgulmlem2  28836  subfacp1lem2a  28888  erdszelem4  28902  erdszelem5  28903  erdszelem7  28905  erdszelem8  28906  kur14lem7  28920  kur14lem9  28922  cvxpcon  28951  cvxscon  28952  rescon  28955  iccllyscon  28959  rprisefaccl  29386  txpss3v  29756  txprel  29757  limitssson  29789  onint1  30142  opnmbllem0  30290  mblfinlem1  30291  mblfinlem2  30292  mblfinlem3  30293  mblfinlem4  30294  ismblfin  30295  mbfposadd  30302  cnambfre  30303  itg2addnc  30309  ftc1cnnclem  30328  ftc1cnnc  30329  ftc1anclem3  30332  ftc1anclem7  30336  ftc1anc  30338  ftc2nc  30339  dvreasin  30345  dvreacos  30346  areacirclem1  30347  areacirclem2  30348  areacirc  30352  finminlem  30376  tailf  30433  filnetlem3  30438  caures  30493  reheibor  30575  diophin  30945  4rexfrabdioph  30971  6rexfrabdioph  30972  irrapxlem1  30997  irrapx1  31003  monotuz  31116  jm2.27dlem5  31194  hbtlem2  31314  algbase  31368  algaddg  31369  algmulr  31370  algsca  31371  algvsca  31372  itgpowd  31423  arearect  31424  areaquad  31425  lhe4.4ex1a  31475  uzmptshftfval  31492  binomcxplemdvbinom  31499  binomcxplemcvg  31500  binomcxplemnotnn0  31502  fzisoeu  31739  fzsscn  31753  fzssre  31757  ioosscn  31766  fprodge0  31836  fprodge1  31837  limcresiooub  31887  limcresioolb  31888  limcleqr  31889  limclner  31896  limclr  31900  icccncfext  31929  cncficcgt0  31930  ioodvbdlimc1lem2  31968  ioodvbdlimc2lem  31970  dvnprodlem1  31982  dvnprodlem2  31983  itgsin0pilem1  31987  itgsinexplem1  31991  itgsinexp  31992  dirkercncflem2  32125  fourierdlem16  32144  fourierdlem18  32146  fourierdlem20  32148  fourierdlem21  32149  fourierdlem22  32150  fourierdlem25  32153  fourierdlem37  32165  fourierdlem42  32170  fourierdlem50  32178  fourierdlem52  32180  fourierdlem62  32190  fourierdlem64  32192  fourierdlem66  32194  fourierdlem68  32196  fourierdlem74  32202  fourierdlem75  32203  fourierdlem76  32204  fourierdlem79  32207  fourierdlem83  32211  fourierdlem95  32223  fourierdlem101  32229  fourierdlem102  32230  fourierdlem103  32231  fourierdlem104  32232  fourierdlem112  32240  fourierdlem114  32242  sqwvfoura  32250  sqwvfourb  32251  fouriersw  32253  etransclem24  32280  etransclem48  32304  oddibas  32873  2zrngbas  32996  2zrng0  32998  aacllem  33604  relopabVD  34102  bnj1145  34450  bnj1286  34476  bj-unrab  34895  bj-2upln1upl  34983  bj-rrvecsscmn  35068  atlatmstc  35441  atlatle  35442  pmaple  35882  sspadd1  35936  sspadd2  35937  taupilem2  38094  taupi  38095  relexpaddss  38205  idhe  38260
  Copyright terms: Public domain W3C validator