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

Theorem sstri 3453
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 3451 . 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 3416
This theorem was proved from axioms:  ax-mp 5  ax-1 6  ax-2 7  ax-3 8  ax-gen 1680  ax-4 1693  ax-5 1769  ax-6 1816  ax-7 1862  ax-10 1926  ax-11 1931  ax-12 1944  ax-13 2102  ax-ext 2442
This theorem depends on definitions:  df-bi 190  df-an 377  df-tru 1458  df-ex 1675  df-nf 1679  df-sb 1809  df-clab 2449  df-cleq 2455  df-clel 2458  df-in 3423  df-ss 3430
This theorem is referenced by:  snsstp1  4136  snsstp2  4137  uniintsn  4286  ssrnres  5297  cossxp  5381  foimacnv  5858  ssimaex  5958  riotassuni  6318  oprabss  6414  dmexg  6756  rnexg  6757  fabexg  6781  fparlem3  6930  fparlem4  6931  snopsuppss  6961  tposssxp  7008  mapsspw  7538  sbthlem5  7717  sbthlem7  7719  cnvimamptfin  7906  marypha1lem  7978  ordtypelem4  8067  hartogslem1  8088  tc2  8257  tz9.12lem1  8289  rankval4  8369  rankxpl  8377  rankmapu  8380  rankxplim  8381  infxpenlem  8475  ackbij1lem18  8698  cflm  8711  fin23lem29  8802  hsmexlem4  8890  hsmexlem5  8891  brdom3  8987  brdom5  8988  brdom4  8989  smobeth  9042  pwfseqlem3  9116  wundm  9184  wunrn  9185  wunex2  9194  ltsopi  9344  dmaddpi  9346  dmmulpi  9347  nqerf  9386  ltrelxr  9726  nnsscn  10647  nn0sscn  10908  uzwo2  11257  uzinfmiOLD  11273  infssuzle  11278  infssuzcl  11279  infmssuzleOLD  11280  infmssuzclOLD  11281  uzwo3  11293  nn0ssq  11306  nnssq  11307  qsscn  11309  rpnnen1lem3  11326  rpnnen1lem5  11328  dflt2  11481  fzval2  11822  fzof  11954  fzossnn  12001  fzo0ssnn0  12031  injresinj  12063  flval3  12088  uzsup  12128  uzrdgfni  12210  expcl2lem  12322  rpexpcl  12329  expge0  12346  expge1  12347  hashxrcl  12577  seqcoll  12666  wrdexg  12721  xptrrel  13099  trclublem  13114  sqrlem3  13363  limsupval2  13595  limsupval2OLD  13596  limsupgre  13597  limsupgreOLD  13598  rlimpm  13619  rlimclim  13665  isercolllem1  13783  isercolllem2  13784  isercoll  13786  caurcvg  13797  caurcvgOLD  13798  caucvg  13800  summolem2a  13836  summolem2  13837  zsum  13839  fsumcvg3  13850  fsumrpcl  13858  fsumge0  13910  climfsum  13935  ackbijnn  13941  prodmolem2a  14043  prodmolem2  14044  zprod  14046  fprodrpcl  14065  fprodge0  14102  fprodge1  14104  rprisefaccl  14131  divalglem8  14435  sadaddlem  14495  lcmfval  14646  lcmfvalOLD  14650  isprm3  14688  maxprmfct  14707  pclem  14843  prmreclem1  14915  prmreclem2  14916  prmreclem3  14917  1arith  14926  4sqlem11  14954  ramtlecl  15006  ramcl2lem  15017  ramcl2lemOLD  15018  ramxrcl  15030  prmgaplem3  15078  prmgaplem4  15079  cshwshashlem1  15121  structfn  15189  strlemor1  15272  strleun  15275  srngbase  15308  srngplusg  15309  srngmulr  15310  lmodbase  15317  lmodplusg  15318  lmodsca  15319  ipsbase  15324  ipsaddg  15325  ipsmulr  15326  ipssca  15327  ipsvsca  15328  ipsip  15329  phlbase  15334  phlplusg  15335  phlsca  15336  phlvsca  15337  phlip  15338  odrngbas  15360  odrngplusg  15361  odrngmulr  15362  odrngtset  15363  odrngle  15364  odrngds  15365  prdsval  15408  prdssca  15409  prdsbas  15410  prdsplusg  15411  prdsmulr  15412  prdsvsca  15413  prdsip  15414  prdsle  15415  prdsds  15417  prdstset  15419  prdshom  15420  prdsco  15421  imasbas  15468  imasds  15469  imasplusg  15473  imasmulr  15474  imassca  15475  imasvsca  15476  imasip  15477  imastset  15478  imasle  15479  imasbasOLD  15480  imasdsOLD  15481  wunfunc  15859  fullfunc  15866  fthfunc  15867  isfull  15870  isfth  15874  wunnat  15916  dmcoass  16016  catcisolem  16056  catciso  16057  catcoppccl  16058  catcfuccl  16059  catcxpccl  16147  ipobas  16456  ipolerval  16457  ipotset  16458  psdmrn  16508  psss  16515  ledm  16525  lern  16526  dirdm  16535  dirge  16538  mvdco  17141  f1omvdconj  17142  gexex  17546  gsumval3  17596  lssacs  18245  asplss  18608  aspsubrg  18610  psrass1lem  18656  psrbas  18657  psrplusg  18660  psrmulr  18663  psrsca  18668  psrvscafval  18669  psrass1  18684  psrass23l  18687  psrcom  18688  psrass23  18689  psropprmul  18886  coe1mul2  18917  cnfldbas  19029  cnfldadd  19030  cnfldmul  19031  cnfldcj  19032  cnfldtset  19033  cnfldle  19034  cnfldds  19035  cnfldunif  19036  rge0srg  19093  zntoslem  19182  ofco2  19531  leordtval2  20283  lmbrf  20331  lmres  20371  fiuncmp  20474  comppfsc  20602  1stckgenlem  20623  kgencn3  20628  ptbasfi  20651  xkoopn  20659  txcnmpt  20694  txkgen  20722  opnfbas  20912  fmfnfmlem4  21027  tsmsxplem1  21222  trust  21299  restutop  21307  nmoffn  21771  nmofval  21774  nmogelb  21776  nmolb  21777  nmof  21779  nmoffnOLD  21792  nmofvalOLD  21793  nmogelbOLD  21795  nmolbOLD  21796  nmofOLD  21797  qtopbas  21835  tgqioo  21873  re2ndc  21874  iitopon  21966  dfii3  21970  iimulcn  22021  cnheiborlem  22037  bndth  22041  lebnumii  22052  reparphti  22083  pcoass  22110  cphsqrtcl  22217  lmmbrf  22287  iscauf  22305  caucfil  22308  lmclimf  22328  rrxmval  22414  rrxmet  22417  ovolfioo  22475  ovolficc  22476  ovolficcss  22477  ovolfsf  22479  ovollb  22487  ovolicc2lem3  22527  ovolicc2lem4OLD  22528  ovolicc2lem4  22529  ovolicc2  22531  volf  22538  volsup  22565  ovolfs2  22579  uniiccdif  22591  uniioovol  22592  uniiccvol  22593  uniioombllem2  22596  uniioombllem2OLD  22597  uniioombllem3a  22598  uniioombllem3  22599  uniioombllem4  22600  uniioombllem5  22601  uniioombl  22603  dyadmbllem  22613  dyadmbl  22614  opnmbllem  22615  opnmblALT  22617  volsup2  22619  vitalilem4  22625  vitalilem5  22626  vitali  22627  mbfimaopnlem  22667  mbflimsup  22679  mbflimsupOLD  22680  i1f0  22701  i1f1  22704  itg11  22705  itg2mulc  22761  itg2gt0  22774  ellimc2  22888  limcresi  22896  dvreslem  22920  dvres2lem  22921  dvaddbr  22948  dvmulbr  22949  dvlipcn  23002  c1liplem1  23004  lhop1lem  23021  lhop1  23022  lhop2  23023  lhop  23024  dvfsumrlim  23039  ftc1cn  23051  itgsubstlem  23056  itgsubst  23057  mdegleb  23069  mdeglt  23070  mdegldg  23071  mdegxrcl  23072  mdegcl  23074  mdegaddle  23079  mdegmullem  23083  deg1mul3le  23121  ig1peu  23178  ig1peuOLD  23179  ig1pdvds  23184  ig1pdvdsOLD  23190  aacjcl  23339  aannenlem2  23341  aannenlem3  23342  aalioulem2  23345  taylfval  23370  radcnvcl  23428  radcnvlt1  23429  radcnvle  23431  abelth  23452  abelth2  23453  pilem2  23463  pilem2OLD  23464  pilem3  23465  pilem3OLD  23466  pige3  23528  recosf1o  23540  resinf1o  23541  tanord1  23542  logcn  23648  dvlog  23652  dvlog2lem  23653  efopn  23659  logtayl  23661  cxpcn3  23744  loglesqrt  23754  ssscongptld  23807  leibpi  23924  efrlim  23951  jensenlem1  23968  jensenlem2  23969  jensen  23970  amgm  23972  lgamgulmlem2  24011  ftalem5  24057  ftalem5OLD  24059  efnnfsumcl  24085  efchtdvds  24142  dvdsmulf1o  24179  fsumdvdsmul  24180  lgsfcl2  24286  2sqlem6  24353  2sqlem8  24356  2sqlem9  24357  rpvmasumlem  24381  rpvmasum2  24406  dchrisum0re  24407  dchrisum0lem3  24413  dchrisum0  24414  rplogsum  24421  dirith2  24422  axtgcgrrflx  24566  axtgcgrid  24567  axtgsegcon  24568  axtg5seg  24569  axtgbtwnid  24570  axtgpasch  24571  axtgcont1  24572  tgcgr4  24632  motcgrg  24645  tglng  24647  umgrass  25102  constr3pthlem1  25439  disjxwwlkn  25529  nmlno0lem  26490  hlimcaui  26945  chsspwh  26956  shsss  27022  chintcli  27040  shsleji  27079  shub1i  27083  shsval2i  27096  lejdii  27247  spanuni  27253  sshhococi  27255  spansnpji  27287  osumcori  27352  5oai  27370  3oalem6  27376  3oai  27377  pjssmii  27390  mayete3i  27437  mayetes3i  27438  nmlnop0iALT  27704  imaelshi  27767  pjnmopi  27857  pjclem1  27904  pjci  27909  mdslmd1lem1  28034  shatomistici  28070  hatomistici  28071  chpssati  28072  xppreima  28301  iundisjfi  28424  iundisj2fi  28425  xrsmulgzz  28492  fsumrp0cl  28509  gsummpt2co  28594  xrge0slmod  28658  unitsscn  28753  ordtconlem1  28781  xrge0iifhom  28794  lmlimxrge0  28805  lmxrge0  28809  esumcst  28935  esumpfinvallem  28946  esumpfinval  28947  esumpfinvalf  28948  esumcvg  28958  imambfm  29134  elmbfmvol2  29139  sxbrsigalem3  29144  sxbrsigalem2  29158  sxbrsigalem4  29159  sitgclg  29225  eulerpartlem1  29250  eulerpartlemgvv  29259  eulerpartlemgh  29261  eulerpartlemgf  29262  ballotlemfc0  29375  ballotlemfcc  29376  ballotlemiex  29384  ballotlemsup  29387  ballotlemsdom  29394  ballotlemsima  29398  ballotlemrv2  29404  ballotth  29420  ballotlemiexOLD  29422  ballotlemsupOLD  29425  ballotlemsdomOLD  29432  ballotlemsimaOLD  29436  ballotlemrv2OLD  29442  ballotthOLD  29458  signsplypnf  29489  signsply0  29490  bnj1145  29852  bnj1286  29878  subfacp1lem2a  29953  erdszelem4  29967  erdszelem5  29968  erdszelem7  29970  erdszelem8  29971  kur14lem7  29985  kur14lem9  29987  cvxpcon  30015  cvxscon  30016  rescon  30019  iccllyscon  30023  txpss3v  30695  txprel  30696  limitssson  30728  finminlem  31024  tailf  31081  filnetlem3  31086  onint1  31159  bj-unrab  31575  bj-2upln1upl  31664  bj-rrvecsscmn  31753  taupilem2  31769  taupi  31770  poimirlem3  31989  poimirlem30  32016  poimirlem31  32017  poimirlem32  32018  broucube  32020  opnmbllem0  32022  mblfinlem1  32023  mblfinlem2  32024  mblfinlem3  32025  mblfinlem4  32026  ismblfin  32027  mbfposadd  32034  cnambfre  32035  itg2addnc  32042  ftc1cnnclem  32061  ftc1cnnc  32062  ftc1anclem3  32065  ftc1anclem7  32069  ftc1anc  32071  ftc2nc  32072  dvreasin  32076  dvreacos  32077  areacirclem1  32078  areacirclem2  32079  areacirc  32083  caures  32135  reheibor  32217  atlatmstc  32931  atlatle  32932  pmaple  33372  sspadd1  33426  sspadd2  33427  diophin  35661  4rexfrabdioph  35687  6rexfrabdioph  35688  irrapxlem1  35712  irrapx1  35718  monotuz  35835  jm2.27dlem5  35914  hbtlem2  36029  algbase  36090  algaddg  36091  algmulr  36092  algsca  36093  algvsca  36094  itgpowd  36145  arearect  36146  areaquad  36147  rtrclex  36270  trclubgNEW  36271  trclexi  36273  rtrclexi  36274  cnvtrcl0  36279  dfrtrcl5  36282  trrelsuperrel2dg  36309  relexpaddss  36356  brtrclfv2  36365  frege131d  36402  xphe  36422  idhe  36429  lhe4.4ex1a  36723  uzmptshftfval  36740  binomcxplemdvbinom  36747  binomcxplemcvg  36748  binomcxplemnotnn0  36750  relopabVD  37339  fzisoeu  37593  fzsscn  37606  fzssre  37610  ioosscn  37676  limcresiooub  37809  limcresioolb  37810  limcleqr  37811  limclner  37818  limclr  37822  icccncfext  37851  cncficcgt0  37852  ioodvbdlimc1lem2  37890  ioodvbdlimc1lem2OLD  37892  ioodvbdlimc2lem  37894  ioodvbdlimc2lemOLD  37895  dvnprodlem1  37907  dvnprodlem2  37908  itgsin0pilem1  37912  itgsinexplem1  37916  itgsinexp  37917  dirkercncflem2  38067  fourierdlem16  38086  fourierdlem18  38088  fourierdlem20  38090  fourierdlem21  38091  fourierdlem22  38092  fourierdlem25  38095  fourierdlem37  38108  fourierdlem42  38113  fourierdlem42OLD  38114  fourierdlem50  38121  fourierdlem52  38123  fourierdlem62  38133  fourierdlem64  38135  fourierdlem66  38137  fourierdlem68  38139  fourierdlem74  38145  fourierdlem75  38146  fourierdlem76  38147  fourierdlem79  38150  fourierdlem83  38154  fourierdlem95  38166  fourierdlem101  38172  fourierdlem102  38173  fourierdlem103  38174  fourierdlem104  38175  fourierdlem112  38183  fourierdlem114  38185  sqwvfoura  38193  sqwvfourb  38194  fouriersw  38196  etransclem24  38224  etransclem48OLD  38248  etransclem48  38249  sge0sn  38324  sge0tsms  38325  sge0f1o  38327  sge0pr  38339  sge0resplit  38351  sge0split  38354  sge0iunmptlemre  38360  sge0isummpt2  38377  carageniuncllem1  38450  hoicvr  38477  hoicvrrex  38485  hoidmvlelem2  38525  hspmbl  38558  upgrss  39323  pthdivtx  39858  oddibas  40182  2zrngbas  40305  2zrng0  40307  aacllem  40909
  Copyright terms: Public domain W3C validator