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

Theorem sstri 3513
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 3511 . 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 3476
This theorem was proved from axioms:  ax-mp 5  ax-1 6  ax-2 7  ax-3 8  ax-gen 1601  ax-4 1612  ax-5 1680  ax-6 1719  ax-7 1739  ax-10 1786  ax-11 1791  ax-12 1803  ax-13 1968  ax-ext 2445
This theorem depends on definitions:  df-bi 185  df-an 371  df-tru 1382  df-ex 1597  df-nf 1600  df-sb 1712  df-clab 2453  df-cleq 2459  df-clel 2462  df-in 3483  df-ss 3490
This theorem is referenced by:  snsstp1  4178  snsstp2  4179  uniintsn  4319  ssrnres  5443  cossxp  5528  foimacnv  5831  ssimaex  5930  riotassuniOLD  6280  oprabss  6370  dmexg  6712  rnexg  6713  fabexg  6737  fparlem3  6882  fparlem4  6883  snopsuppss  6913  tposssxp  6956  mapsspw  7451  sbthlem5  7628  sbthlem7  7630  cnvimamptfin  7817  marypha1lem  7889  ordtypelem4  7942  hartogslem1  7963  tc2  8169  tz9.12lem1  8201  rankval4  8281  rankxpl  8289  rankmapu  8292  rankxplim  8293  infxpenlem  8387  ackbij1lem18  8613  cflm  8626  fin23lem29  8717  hsmexlem4  8805  hsmexlem5  8806  brdom3  8902  brdom5  8903  brdom4  8904  smobeth  8957  pwfseqlem3  9034  wundm  9102  wunrn  9103  wunex2  9112  ltsopi  9262  dmaddpi  9264  dmmulpi  9265  nqerf  9304  ltrelxr  9644  nnsscn  10537  nn0sscn  10796  uzwo2  11142  uzinfmi  11157  infmssuzle  11160  infmssuzcl  11161  uzwo3  11173  nn0ssq  11186  nnssq  11187  qsscn  11189  rpnnen1lem3  11206  rpnnen1lem5  11208  dflt2  11350  fzval2  11671  fzof  11790  fzossnn  11834  fzo0ssnn0  11860  injresinj  11890  flval3  11915  uzsup  11954  uzrdgfni  12033  expcl2lem  12142  rpexpcl  12149  expge0  12166  expge1  12167  hashxrcl  12393  seqcoll  12474  wrdexg  12519  seqshft  12877  sqrlem3  13037  limsupval2  13262  limsupgre  13263  rlimpm  13282  rlimclim  13328  isercolllem1  13446  isercolllem2  13447  isercoll  13449  caurcvg  13458  caucvg  13460  summolem2a  13496  summolem2  13497  zsum  13499  fsumcvg3  13510  fsumrpcl  13518  fsumge0  13568  climfsum  13593  ackbijnn  13599  divalglem8  13913  sadaddlem  13971  isprm3  14081  maxprmfct  14109  pclem  14217  prmreclem1  14289  prmreclem2  14290  prmreclem3  14291  1arith  14300  4sqlem11  14328  ramtlecl  14373  ramcl2lem  14382  ramxrcl  14390  cshwshashlem1  14434  structfn  14499  strlemor1  14578  strleun  14581  srngbase  14607  srngplusg  14608  srngmulr  14609  lmodbase  14616  lmodplusg  14617  lmodsca  14618  ipsbase  14623  ipsaddg  14624  ipsmulr  14625  ipssca  14626  ipsvsca  14627  ipsip  14628  phlbase  14633  phlplusg  14634  phlsca  14635  phlvsca  14636  phlip  14637  odrngbas  14659  odrngplusg  14660  odrngmulr  14661  odrngtset  14662  odrngle  14663  odrngds  14664  prdsval  14706  prdssca  14707  prdsbas  14708  prdsplusg  14709  prdsmulr  14710  prdsvsca  14711  prdsip  14712  prdsle  14713  prdsds  14715  prdstset  14717  prdshom  14718  prdsco  14719  imasbas  14763  imasds  14764  imasplusg  14768  imasmulr  14769  imassca  14770  imasvsca  14771  imasip  14772  imastset  14773  imasle  14774  wunfunc  15122  fullfunc  15129  fthfunc  15130  isfull  15133  isfth  15137  wunnat  15179  dmcoass  15247  catcisolem  15287  catciso  15288  catcoppccl  15289  catcfuccl  15290  catcxpccl  15330  ipobas  15638  ipolerval  15639  ipotset  15640  psdmrn  15690  psss  15697  ledm  15707  lern  15708  dirdm  15717  dirge  15720  mvdco  16266  f1omvdconj  16267  gexex  16652  gsumval3OLD  16699  gsumval3  16702  gsumzaddlemOLD  16727  lssacs  17396  asplss  17749  aspsubrg  17751  psrass1lem  17800  psrbas  17801  psrbasOLD  17802  psrplusg  17805  psrmulr  17808  psrsca  17813  psrvscafval  17814  psrass1  17831  psrdi  17832  psrdir  17833  psrass23l  17834  psrcom  17835  psrass23  17836  psropprmul  18050  coe1mul2  18081  cnfldbas  18195  cnfldadd  18196  cnfldmul  18197  cnfldcj  18198  cnfldtset  18199  cnfldle  18200  cnfldds  18201  cnfldunif  18202  rge0srg  18255  zntoslem  18362  ofco2  18720  leordtval2  19479  lmbrf  19527  lmres  19567  fiuncmp  19670  1stckgenlem  19789  kgencn3  19794  ptbasfi  19817  xkoopn  19825  txcnmpt  19860  txkgen  19888  opnfbas  20078  fmfnfmlem4  20193  tsmsxplem1  20390  trust  20467  restutop  20475  nmoffn  20953  nmofval  20956  nmogelb  20958  nmolb  20959  nmof  20961  qtopbas  21001  tgqioo  21040  re2ndc  21041  iitopon  21118  dfii3  21122  iimulcn  21173  cnheiborlem  21189  bndth  21193  lebnumii  21201  reparphti  21232  pcoass  21259  cphsqrtcl  21366  lmmbrf  21436  iscauf  21454  caucfil  21457  lmclimf  21477  rrxmval  21567  rrxmet  21570  ovolfioo  21614  ovolficc  21615  ovolficcss  21616  ovolfsf  21618  ovollb  21625  ovolicc2lem3  21665  ovolicc2lem4  21666  ovolicc2  21668  volf  21675  volsup  21701  ovolfs2  21715  uniiccdif  21722  uniioovol  21723  uniiccvol  21724  uniioombllem2  21727  uniioombllem3a  21728  uniioombllem3  21729  uniioombllem4  21730  uniioombllem5  21731  uniioombl  21733  dyadmbllem  21743  dyadmbl  21744  opnmbllem  21745  opnmblALT  21747  volsup2  21749  vitalilem4  21755  vitalilem5  21756  vitali  21757  mbfimaopnlem  21797  mbflimsup  21808  i1f0  21829  i1f1  21832  itg11  21833  itg2mulc  21889  itg2gt0  21902  ellimc2  22016  limcresi  22024  dvreslem  22048  dvres2lem  22049  dvaddbr  22076  dvmulbr  22077  dvlipcn  22130  c1liplem1  22132  lhop1lem  22149  lhop1  22150  lhop2  22151  lhop  22152  dvfsumrlim  22167  ftc1cn  22179  itgsubstlem  22184  itgsubst  22185  mdegleb  22199  mdeglt  22200  mdegldg  22201  mdegxrcl  22202  mdegcl  22204  mdegaddle  22209  mdegmullem  22213  deg1mul3le  22252  ig1peu  22307  ig1pdvds  22312  aacjcl  22457  aannenlem2  22459  aannenlem3  22460  aalioulem2  22463  taylfval  22488  radcnvcl  22546  radcnvlt1  22547  radcnvle  22549  abelth  22570  abelth2  22571  pilem2  22581  pilem3  22582  pige3  22643  recosf1o  22655  resinf1o  22656  tanord1  22657  logcn  22756  dvlog  22760  dvlog2lem  22761  efopn  22767  logtayl  22769  cxpcn3  22850  loglesqrt  22860  ssscongptld  22884  leibpi  23001  efrlim  23027  jensenlem1  23044  jensenlem2  23045  jensen  23046  amgm  23048  ftalem5  23078  efnnfsumcl  23104  efchtdvds  23161  dvdsmulf1o  23198  fsumdvdsmul  23199  lgsfcl2  23305  2sqlem6  23372  2sqlem8  23375  2sqlem9  23376  rpvmasumlem  23400  rpvmasum2  23425  dchrisum0re  23426  dchrisum0lem3  23432  dchrisum0  23433  rplogsum  23440  dirith2  23441  axtgcgrrflx  23587  axtgcgrid  23588  axtgsegcon  23589  axtg5seg  23590  axtgbtwnid  23591  axtgpasch  23592  axtgcont1  23593  motcgrg  23659  tglng  23661  umgrass  23995  constr3pthlem1  24331  disjxwwlkn  24421  nmlno0lem  25384  hlimcaui  25830  chsspwh  25841  shsss  25907  chintcli  25925  shsleji  25964  shub1i  25968  shsval2i  25981  lejdii  26132  spanuni  26138  sshhococi  26140  spansnpji  26172  osumcori  26237  5oai  26255  3oalem6  26261  3oai  26262  pjssmii  26275  mayete3i  26322  mayete3iOLD  26323  mayetes3i  26324  nmlnop0iALT  26590  imaelshi  26653  pjnmopi  26743  pjclem1  26790  pjci  26795  mdslmd1lem1  26920  shatomistici  26956  hatomistici  26957  chpssati  26958  xppreima  27159  iundisjfi  27269  iundisj2fi  27270  xrsmulgzz  27328  fsumrp0cl  27347  gsummpt2co  27434  xrge0slmod  27497  unitsscn  27514  ordtconlem1  27542  xrge0iifhom  27555  lmlimxrge0  27566  lmxrge0  27570  esumcst  27711  esumpfinvallem  27720  esumpfinval  27721  esumpfinvalf  27722  esumcvg  27732  measunl  27827  imambfm  27873  elmbfmvol2  27878  sxbrsigalem3  27883  sxbrsigalem2  27897  sxbrsigalem4  27898  sitgclg  27924  eulerpartlem1  27946  eulerpartlemgvv  27955  eulerpartlemgh  27957  eulerpartlemgf  27958  ballotlemfc0  28071  ballotlemfcc  28072  ballotlemiex  28080  ballotlemsup  28083  ballotlemsdom  28090  ballotlemsima  28094  ballotlemrv2  28100  ballotth  28116  signsplypnf  28147  signsply0  28148  lgamgulmlem2  28212  subfacp1lem2a  28264  erdszelem4  28278  erdszelem5  28279  erdszelem7  28281  erdszelem8  28282  kur14lem7  28296  kur14lem9  28298  cvxpcon  28327  cvxscon  28328  rescon  28331  iccllyscon  28335  prodmolem2a  28643  prodmolem2  28644  zprod  28646  fprodrpcl  28665  rprisefaccl  28722  txpss3v  29105  txprel  29106  limitssson  29138  onint1  29491  opnmbllem0  29627  mblfinlem1  29628  mblfinlem2  29629  mblfinlem3  29630  mblfinlem4  29631  ismblfin  29632  mbfposadd  29639  cnambfre  29640  itg2addnc  29646  ftc1cnnclem  29665  ftc1cnnc  29666  ftc1anclem3  29669  ftc1anclem7  29673  ftc1anc  29675  ftc2nc  29676  dvreasin  29682  dvreacos  29683  areacirclem1  29684  areacirclem2  29685  areacirc  29689  finminlem  29713  comppfsc  29779  tailf  29796  filnetlem3  29801  caures  29856  reheibor  29938  diophin  30310  4rexfrabdioph  30335  6rexfrabdioph  30336  irrapxlem1  30362  irrapx1  30368  monotuz  30481  jm2.27dlem5  30559  hbtlem2  30677  algbase  30732  algaddg  30733  algmulr  30734  algsca  30735  algvsca  30736  itgpowd  30787  arearect  30788  areaquad  30789  lhe4.4ex1a  30834  fzisoeu  31077  ioosscn  31091  limcresiooub  31184  limcresioolb  31185  limcleqr  31186  limclner  31193  limclr  31197  cncficcgt0  31227  cncfiooicclem1  31232  dvmptresicc  31249  ioodvbdlimc1lem2  31262  ioodvbdlimc2lem  31264  itgsin0pilem1  31267  itgsinexplem1  31271  itgsinexp  31272  itgsbtaddcnst  31300  wallispilem2  31366  dirkeritg  31402  dirkercncflem2  31404  fourierdlem16  31423  fourierdlem18  31425  fourierdlem20  31427  fourierdlem21  31428  fourierdlem22  31429  fourierdlem25  31432  fourierdlem37  31444  fourierdlem40  31447  fourierdlem42  31449  fourierdlem50  31457  fourierdlem52  31459  fourierdlem57  31464  fourierdlem62  31469  fourierdlem64  31471  fourierdlem66  31473  fourierdlem68  31475  fourierdlem74  31481  fourierdlem75  31482  fourierdlem76  31483  fourierdlem78  31485  fourierdlem79  31486  fourierdlem83  31490  fourierdlem93  31500  fourierdlem95  31502  fourierdlem101  31508  fourierdlem102  31509  fourierdlem103  31510  fourierdlem104  31511  fourierdlem111  31518  fourierdlem112  31519  fourierdlem114  31521  sqwvfoura  31529  sqwvfourb  31530  fouriersw  31532  relopabVD  32781  bnj1145  33128  bnj1286  33154  bj-unrab  33575  bj-2upln1upl  33663  bj-rrvecsscmn  33740  atlatmstc  34116  atlatle  34117  pmaple  34557  sspadd1  34611  sspadd2  34612  taupilem2  36768  taupi  36769  xptrrel  36785  trclubg  36795
  Copyright terms: Public domain W3C validator