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

Theorem sstri 3496
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 3494 . 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 3459
This theorem was proved from axioms:  ax-mp 5  ax-1 6  ax-2 7  ax-3 8  ax-gen 1603  ax-4 1616  ax-5 1689  ax-6 1732  ax-7 1774  ax-10 1821  ax-11 1826  ax-12 1838  ax-13 1983  ax-ext 2419
This theorem depends on definitions:  df-bi 185  df-an 371  df-tru 1384  df-ex 1598  df-nf 1602  df-sb 1725  df-clab 2427  df-cleq 2433  df-clel 2436  df-in 3466  df-ss 3473
This theorem is referenced by:  snsstp1  4163  snsstp2  4164  uniintsn  4306  ssrnres  5432  cossxp  5517  foimacnv  5820  ssimaex  5920  riotassuniOLD  6276  oprabss  6370  dmexg  6713  rnexg  6714  fabexg  6738  fparlem3  6884  fparlem4  6885  snopsuppss  6915  tposssxp  6958  mapsspw  7453  sbthlem5  7630  sbthlem7  7632  cnvimamptfin  7820  marypha1lem  7892  ordtypelem4  7946  hartogslem1  7967  tc2  8173  tz9.12lem1  8205  rankval4  8285  rankxpl  8293  rankmapu  8296  rankxplim  8297  infxpenlem  8391  ackbij1lem18  8617  cflm  8630  fin23lem29  8721  hsmexlem4  8809  hsmexlem5  8810  brdom3  8906  brdom5  8907  brdom4  8908  smobeth  8961  pwfseqlem3  9038  wundm  9106  wunrn  9107  wunex2  9116  ltsopi  9266  dmaddpi  9268  dmmulpi  9269  nqerf  9308  ltrelxr  9648  nnsscn  10544  nn0sscn  10803  uzwo2  11152  uzinfmi  11167  infmssuzle  11170  infmssuzcl  11171  uzwo3  11183  nn0ssq  11196  nnssq  11197  qsscn  11199  rpnnen1lem3  11216  rpnnen1lem5  11218  dflt2  11360  fzval2  11681  fzof  11802  fzossnn  11846  fzo0ssnn0  11872  injresinj  11902  flval3  11927  uzsup  11966  uzrdgfni  12045  expcl2lem  12154  rpexpcl  12161  expge0  12178  expge1  12179  hashxrcl  12405  seqcoll  12488  wrdexg  12533  sqrlem3  13054  limsupval2  13279  limsupgre  13280  rlimpm  13299  rlimclim  13345  isercolllem1  13463  isercolllem2  13464  isercoll  13466  caurcvg  13475  caucvg  13477  summolem2a  13513  summolem2  13514  zsum  13516  fsumcvg3  13527  fsumrpcl  13535  fsumge0  13585  climfsum  13610  ackbijnn  13616  divalglem8  13932  sadaddlem  13990  isprm3  14100  maxprmfct  14128  pclem  14236  prmreclem1  14308  prmreclem2  14309  prmreclem3  14310  1arith  14319  4sqlem11  14347  ramtlecl  14392  ramcl2lem  14401  ramxrcl  14409  cshwshashlem1  14454  structfn  14519  strlemor1  14598  strleun  14601  srngbase  14627  srngplusg  14628  srngmulr  14629  lmodbase  14636  lmodplusg  14637  lmodsca  14638  ipsbase  14643  ipsaddg  14644  ipsmulr  14645  ipssca  14646  ipsvsca  14647  ipsip  14648  phlbase  14653  phlplusg  14654  phlsca  14655  phlvsca  14656  phlip  14657  odrngbas  14679  odrngplusg  14680  odrngmulr  14681  odrngtset  14682  odrngle  14683  odrngds  14684  prdsval  14726  prdssca  14727  prdsbas  14728  prdsplusg  14729  prdsmulr  14730  prdsvsca  14731  prdsip  14732  prdsle  14733  prdsds  14735  prdstset  14737  prdshom  14738  prdsco  14739  imasbas  14783  imasds  14784  imasplusg  14788  imasmulr  14789  imassca  14790  imasvsca  14791  imasip  14792  imastset  14793  imasle  14794  wunfunc  15139  fullfunc  15146  fthfunc  15147  isfull  15150  isfth  15154  wunnat  15196  dmcoass  15264  catcisolem  15304  catciso  15305  catcoppccl  15306  catcfuccl  15307  catcxpccl  15347  ipobas  15656  ipolerval  15657  ipotset  15658  psdmrn  15708  psss  15715  ledm  15725  lern  15726  dirdm  15735  dirge  15738  mvdco  16341  f1omvdconj  16342  gexex  16730  gsumval3OLD  16779  gsumval3  16782  gsumzaddlemOLD  16807  lssacs  17484  asplss  17849  aspsubrg  17851  psrass1lem  17900  psrbas  17901  psrbasOLD  17902  psrplusg  17905  psrmulr  17908  psrsca  17913  psrvscafval  17914  psrass1  17931  psrass23l  17934  psrcom  17935  psrass23  17936  psropprmul  18150  coe1mul2  18181  cnfldbas  18295  cnfldadd  18296  cnfldmul  18297  cnfldcj  18298  cnfldtset  18299  cnfldle  18300  cnfldds  18301  cnfldunif  18302  rge0srg  18358  zntoslem  18465  ofco2  18823  leordtval2  19583  lmbrf  19631  lmres  19671  fiuncmp  19774  comppfsc  19903  1stckgenlem  19924  kgencn3  19929  ptbasfi  19952  xkoopn  19960  txcnmpt  19995  txkgen  20023  opnfbas  20213  fmfnfmlem4  20328  tsmsxplem1  20525  trust  20602  restutop  20610  nmoffn  21088  nmofval  21091  nmogelb  21093  nmolb  21094  nmof  21096  qtopbas  21136  tgqioo  21175  re2ndc  21176  iitopon  21253  dfii3  21257  iimulcn  21308  cnheiborlem  21324  bndth  21328  lebnumii  21336  reparphti  21367  pcoass  21394  cphsqrtcl  21501  lmmbrf  21571  iscauf  21589  caucfil  21592  lmclimf  21612  rrxmval  21702  rrxmet  21705  ovolfioo  21749  ovolficc  21750  ovolficcss  21751  ovolfsf  21753  ovollb  21760  ovolicc2lem3  21800  ovolicc2lem4  21801  ovolicc2  21803  volf  21810  volsup  21836  ovolfs2  21850  uniiccdif  21857  uniioovol  21858  uniiccvol  21859  uniioombllem2  21862  uniioombllem3a  21863  uniioombllem3  21864  uniioombllem4  21865  uniioombllem5  21866  uniioombl  21868  dyadmbllem  21878  dyadmbl  21879  opnmbllem  21880  opnmblALT  21882  volsup2  21884  vitalilem4  21890  vitalilem5  21891  vitali  21892  mbfimaopnlem  21932  mbflimsup  21943  i1f0  21964  i1f1  21967  itg11  21968  itg2mulc  22024  itg2gt0  22037  ellimc2  22151  limcresi  22159  dvreslem  22183  dvres2lem  22184  dvaddbr  22211  dvmulbr  22212  dvlipcn  22265  c1liplem1  22267  lhop1lem  22284  lhop1  22285  lhop2  22286  lhop  22287  dvfsumrlim  22302  ftc1cn  22314  itgsubstlem  22319  itgsubst  22320  mdegleb  22334  mdeglt  22335  mdegldg  22336  mdegxrcl  22337  mdegcl  22339  mdegaddle  22344  mdegmullem  22348  deg1mul3le  22387  ig1peu  22442  ig1pdvds  22447  aacjcl  22592  aannenlem2  22594  aannenlem3  22595  aalioulem2  22598  taylfval  22623  radcnvcl  22681  radcnvlt1  22682  radcnvle  22684  abelth  22705  abelth2  22706  pilem2  22716  pilem3  22717  pige3  22779  recosf1o  22791  resinf1o  22792  tanord1  22793  logcn  22897  dvlog  22901  dvlog2lem  22902  efopn  22908  logtayl  22910  cxpcn3  22991  loglesqrt  23001  ssscongptld  23025  leibpi  23142  efrlim  23168  jensenlem1  23185  jensenlem2  23186  jensen  23187  amgm  23189  ftalem5  23219  efnnfsumcl  23245  efchtdvds  23302  dvdsmulf1o  23339  fsumdvdsmul  23340  lgsfcl2  23446  2sqlem6  23513  2sqlem8  23516  2sqlem9  23517  rpvmasumlem  23541  rpvmasum2  23566  dchrisum0re  23567  dchrisum0lem3  23573  dchrisum0  23574  rplogsum  23581  dirith2  23582  axtgcgrrflx  23728  axtgcgrid  23729  axtgsegcon  23730  axtg5seg  23731  axtgbtwnid  23732  axtgpasch  23733  axtgcont1  23734  motcgrg  23800  tglng  23802  umgrass  24188  constr3pthlem1  24524  disjxwwlkn  24614  nmlno0lem  25577  hlimcaui  26023  chsspwh  26034  shsss  26100  chintcli  26118  shsleji  26157  shub1i  26161  shsval2i  26174  lejdii  26325  spanuni  26331  sshhococi  26333  spansnpji  26365  osumcori  26430  5oai  26448  3oalem6  26454  3oai  26455  pjssmii  26468  mayete3i  26515  mayete3iOLD  26516  mayetes3i  26517  nmlnop0iALT  26783  imaelshi  26846  pjnmopi  26936  pjclem1  26983  pjci  26988  mdslmd1lem1  27113  shatomistici  27149  hatomistici  27150  chpssati  27151  xppreima  27356  iundisjfi  27470  iundisj2fi  27471  xrsmulgzz  27536  fsumrp0cl  27555  gsummpt2co  27641  xrge0slmod  27704  unitsscn  27748  ordtconlem1  27776  xrge0iifhom  27789  lmlimxrge0  27800  lmxrge0  27804  esumcst  27941  esumpfinvallem  27950  esumpfinval  27951  esumpfinvalf  27952  esumcvg  27962  imambfm  28103  elmbfmvol2  28108  sxbrsigalem3  28113  sxbrsigalem2  28127  sxbrsigalem4  28128  sitgclg  28154  eulerpartlem1  28176  eulerpartlemgvv  28185  eulerpartlemgh  28187  eulerpartlemgf  28188  ballotlemfc0  28301  ballotlemfcc  28302  ballotlemiex  28310  ballotlemsup  28313  ballotlemsdom  28320  ballotlemsima  28324  ballotlemrv2  28330  ballotth  28346  signsplypnf  28377  signsply0  28378  lgamgulmlem2  28442  subfacp1lem2a  28494  erdszelem4  28508  erdszelem5  28509  erdszelem7  28511  erdszelem8  28512  kur14lem7  28526  kur14lem9  28528  cvxpcon  28557  cvxscon  28558  rescon  28561  iccllyscon  28565  prodmolem2a  29038  prodmolem2  29039  zprod  29041  fprodrpcl  29060  rprisefaccl  29117  txpss3v  29500  txprel  29501  limitssson  29533  onint1  29886  opnmbllem0  30022  mblfinlem1  30023  mblfinlem2  30024  mblfinlem3  30025  mblfinlem4  30026  ismblfin  30027  mbfposadd  30034  cnambfre  30035  itg2addnc  30041  ftc1cnnclem  30060  ftc1cnnc  30061  ftc1anclem3  30064  ftc1anclem7  30068  ftc1anc  30070  ftc2nc  30071  dvreasin  30077  dvreacos  30078  areacirclem1  30079  areacirclem2  30080  areacirc  30084  finminlem  30108  tailf  30165  filnetlem3  30170  caures  30225  reheibor  30307  diophin  30678  4rexfrabdioph  30703  6rexfrabdioph  30704  irrapxlem1  30730  irrapx1  30736  monotuz  30849  jm2.27dlem5  30927  hbtlem2  31045  algbase  31100  algaddg  31101  algmulr  31102  algsca  31103  algvsca  31104  itgpowd  31155  arearect  31156  areaquad  31157  lhe4.4ex1a  31207  fzisoeu  31449  ioosscn  31463  limcresiooub  31556  limcresioolb  31557  limcleqr  31558  limclner  31565  limclr  31569  icccncfext  31597  cncficcgt0  31598  ioodvbdlimc1lem2  31633  ioodvbdlimc2lem  31635  itgsin0pilem1  31638  itgsinexplem1  31642  itgsinexp  31643  dirkercncflem2  31775  fourierdlem16  31794  fourierdlem18  31796  fourierdlem20  31798  fourierdlem21  31799  fourierdlem22  31800  fourierdlem25  31803  fourierdlem37  31815  fourierdlem42  31820  fourierdlem50  31828  fourierdlem52  31830  fourierdlem62  31840  fourierdlem64  31842  fourierdlem66  31844  fourierdlem68  31846  fourierdlem74  31852  fourierdlem75  31853  fourierdlem76  31854  fourierdlem79  31857  fourierdlem83  31861  fourierdlem95  31873  fourierdlem101  31879  fourierdlem102  31880  fourierdlem103  31881  fourierdlem104  31882  fourierdlem112  31890  fourierdlem114  31892  sqwvfoura  31900  sqwvfourb  31901  fouriersw  31903  oddibas  32338  2zrngbas  32449  2zrng0  32451  relopabVD  33429  bnj1145  33777  bnj1286  33803  bj-unrab  34227  bj-2upln1upl  34315  bj-rrvecsscmn  34391  atlatmstc  34767  atlatle  34768  pmaple  35208  sspadd1  35262  sspadd2  35263  taupilem2  37420  taupi  37421  xptrrel  37451  trclubg  37461  idhe  37480
  Copyright terms: Public domain W3C validator