Theorem sstri 3943

Description: Subclass transitivity inference. (Contributed by NM, 5-May-2000.)

Hypotheses

Ref	Expression
sstri.1	⊢ 𝐴 ⊆ 𝐵
sstri.2	⊢ 𝐵 ⊆ 𝐶

Assertion

Ref	Expression
sstri	⊢ 𝐴 ⊆ 𝐶

Proof of Theorem sstri

Step	Hyp	Ref	Expression
1		sstri.1	. 2 ⊢ 𝐴 ⊆ 𝐵
2		sstri.2	. 2 ⊢ 𝐵 ⊆ 𝐶
3		sstr2 3940	. 2 ⊢ (𝐴 ⊆ 𝐵 → (𝐵 ⊆ 𝐶 → 𝐴 ⊆ 𝐶))
4	1, 2, 3	mp2 9	1 ⊢ 𝐴 ⊆ 𝐶

Syntax hints:   ⊆ wss 3901

This theorem was proved from axioms:  ax-mp 5  ax-1 6  ax-2 7  ax-3 8  ax-gen 1796  ax-4 1810

This theorem depends on definitions:  df-bi 207  df-ss 3918

This theorem is referenced by:  snsstp1  4772  snsstp2  4773  uniintsn  4940  elopabran  5509  ssrnres  6136  cossxp  6230  foimacnv  6791  ssimaex  6919  riotassuni  7355  oprabss  7466  dmexg  7843  rnexg  7844  fabexgOLD  7881  mptmpoopabbrd  8024  fparlem3  8056  fparlem4  8057  snopsuppss  8121  tposssxp  8172  naddunif  8621  naddasslem1  8622  naddasslem2  8623  mapsspw  8816  sbthlem5  9019  sbthlem7  9021  cnvimamptfin  9253  marypha1lem  9336  ordtypelem4  9426  hartogslem1  9447  ttrclco  9627  cottrcl  9628  tc2  9649  frmin  9661  frrlem16  9670  tz9.12lem1  9699  rankval4  9779  rankxpl  9787  rankmapu  9790  rankxplim  9791  djuin  9830  infxpenlem  9923  ackbij1lem18  10146  cflm  10160  fin23lem29  10251  hsmexlem4  10339  hsmexlem5  10340  brdom3  10438  brdom5  10439  brdom4  10440  smobeth  10497  pwfseqlem3  10571  wundm  10639  wunrn  10640  wunex2  10649  ltsopi  10799  dmaddpi  10801  dmmulpi  10802  nqerf  10841  ltrelxr  11193  uzssre  12773  uzwo2  12825  infssuzle  12844  infssuzcl  12845  uzwo3  12856  nn0ssq  12870  nnssq  12871  qsscn  12873  rpnnen1lem3  12892  rpnnen1lem5  12894  dflt2  13062  ioosscn  13324  unitsscn  13416  fzval2  13426  fzossz  13595  fzossnn  13627  injresinj  13707  flval3  13735  uzsup  13783  uzrdgfni  13881  expcl2lem  13996  rpexpcl  14003  expge0  14021  expge1  14022  hashxrcl  14280  seqcoll  14387  xptrrel  14903  trclublem  14918  01sqrexlem3  15167  limsupval2  15403  limsupgre  15404  rlimpm  15423  rlimclim  15469  isercolllem1  15588  isercolllem2  15589  isercoll  15591  caurcvg  15600  caucvg  15602  summolem2a  15638  summolem2  15639  zsum  15641  fsumcvg3  15652  fsumrpcl  15660  fsumge0  15718  climfsum  15743  ackbijnn  15751  prodmolem2a  15857  prodmolem2  15858  zprod  15860  fprodrpcl  15879  fprodge0  15916  fprodge1  15918  rprisefaccl  15946  divalglem8  16327  sadaddlem  16393  lcmfval  16548  isprm3  16610  maxprmfct  16636  pclem  16766  prmreclem1  16844  prmreclem2  16845  prmreclem3  16846  1arith  16855  4sqlem11  16883  ramtlecl  16928  ramcl2lem  16937  ramxrcl  16945  prmgaplem3  16981  prmgaplem4  16982  cshwshashlem1  17023  structfn  17083  strleun  17084  ressbasss  17166  ressbasss2  17168  srngbase  17230  srngplusg  17231  srngmulr  17232  lmodbase  17246  lmodplusg  17247  lmodsca  17248  ipsbase  17257  ipsaddg  17258  ipsmulr  17259  ipssca  17260  ipsvsca  17261  ipsip  17262  phlbase  17267  phlplusg  17268  phlsca  17269  phlvsca  17270  phlip  17271  odrngbas  17324  odrngplusg  17325  odrngmulr  17326  odrngtset  17327  odrngle  17328  odrngds  17329  prdsvallem  17374  prdsval  17375  prdssca  17376  prdsbas  17377  prdsplusg  17378  prdsmulr  17379  prdsvsca  17380  prdsip  17381  prdsle  17382  prdsds  17384  prdstset  17386  prdshom  17387  prdsco  17388  imasbas  17433  imasds  17434  imasplusg  17438  imasmulr  17439  imassca  17440  imasvsca  17441  imasip  17442  imastset  17443  imasle  17444  wunfunc  17825  fullfunc  17832  fthfunc  17833  isfull  17836  isfth  17840  wunnat  17883  dmcoass  17990  catcisolem  18034  catciso  18035  catcoppccl  18041  catcfuccl  18042  catcxpccl  18130  ipobas  18454  ipolerval  18455  ipotset  18456  psdmrn  18496  psss  18503  ledm  18513  lern  18514  dirdm  18523  dirge  18526  mulgfval  18999  mvdco  19374  f1omvdconj  19375  gexex  19782  gsumval3  19836  lssacs  20918  cnfldbas  21313  mpocnfldadd  21314  mpocnfldmul  21316  cnfldcj  21318  cnfldtset  21319  cnfldle  21320  cnfldds  21321  cnfldunif  21322  cnfldbasOLD  21328  cnfldaddOLD  21329  cnfldmulOLD  21330  cnfldcjOLD  21331  cnfldtsetOLD  21332  cnfldleOLD  21333  cnflddsOLD  21334  cnfldunifOLD  21335  rge0srg  21393  zntoslem  21511  asplss  21829  aspsubrg  21831  psrass1lem  21888  psrbas  21889  psrplusg  21892  psrmulr  21898  psrsca  21903  psrvscafval  21904  psrass1  21919  psrass23l  21922  psrcom  21923  psrass23  21924  psropprmul  22178  coe1mul2  22211  ofco2  22395  toponsspwpw  22866  dmtopon  22867  leordtval2  23156  lmbrf  23204  lmres  23244  fiuncmp  23348  comppfsc  23476  1stckgenlem  23497  kgencn3  23502  ptbasfi  23525  xkoopn  23533  txcnmpt  23568  txkgen  23596  opnfbas  23786  fmfnfmlem4  23901  tsmsxplem1  24097  trust  24173  restutop  24181  nmoffn  24655  nmofval  24658  nmogelb  24660  nmolb  24661  nmof  24663  qtopbas  24703  tgqioo  24744  re2ndc  24745  iitopon  24828  dfii3  24832  iimulcnOLD  24891  cnheiborlem  24909  bndth  24913  lebnumii  24921  reparphtiOLD  24953  pcoass  24980  cphsqrtcl  25140  lmmbrf  25218  iscauf  25236  caucfil  25239  lmclimf  25260  rrxmval  25361  rrxmet  25364  ovolfioo  25424  ovolficc  25425  ovolficcss  25426  ovolfsf  25428  ovollb  25436  ovolicc2lem3  25476  ovolicc2lem4  25477  ovolicc2  25479  volf  25486  volsup  25513  ovolfs2  25528  uniiccdif  25535  uniioovol  25536  uniiccvol  25537  uniioombllem2  25540  uniioombllem3a  25541  uniioombllem3  25542  uniioombllem4  25543  uniioombllem5  25544  uniioombl  25546  dyadmbllem  25556  dyadmbl  25557  opnmbllem  25558  opnmblALT  25560  volsup2  25562  vitalilem4  25568  vitalilem5  25569  vitali  25570  mbfimaopnlem  25612  mbflimsup  25623  i1f0  25644  i1f1  25647  itg11  25648  itg2mulc  25704  itg2gt0  25717  ellimc2  25834  limcresi  25842  dvreslem  25866  dvres2lem  25867  dvaddbr  25896  dvmulbr  25897  dvmulbrOLD  25898  dvlipcn  25955  c1liplem1  25957  lhop1lem  25974  lhop1  25975  lhop2  25976  lhop  25977  dvfsumrlim  25994  ftc1cn  26006  itgsubstlem  26011  itgsubst  26012  itgpowd  26013  mdegleb  26025  mdeglt  26026  mdegldg  26027  mdegxrcl  26028  mdegcl  26030  mdegaddle  26035  mdegmullem  26039  deg1mul3le  26078  ig1peu  26136  ig1pdvds  26141  aacjcl  26291  aannenlem2  26293  aannenlem3  26294  aalioulem2  26297  taylfval  26322  radcnvcl  26382  radcnvlt1  26383  radcnvle  26385  abelth  26407  abelth2  26408  pilem2  26418  pilem3  26419  pige3ALT  26485  recosf1o  26500  resinf1o  26501  tanord1  26502  logcn  26612  dvlog  26616  dvlog2lem  26617  efopn  26623  logtayl  26625  cxpcn3  26714  loglesqrt  26727  ssscongptld  26788  leibpi  26908  efrlim  26935  efrlimOLD  26936  jensenlem1  26953  jensenlem2  26954  jensen  26955  amgm  26957  lgamgulmlem2  26996  ftalem5  27043  efnnfsumcl  27069  efchtdvds  27125  mpodvdsmulf1o  27160  fsumdvdsmul  27161  dvdsmulf1o  27162  fsumdvdsmulOLD  27163  lgsfcl2  27270  2sqlem6  27390  2sqlem8  27393  2sqlem9  27394  rpvmasumlem  27454  rpvmasum2  27479  dchrisum0re  27480  dchrisum0lem3  27486  dchrisum0  27487  rplogsum  27494  dirith2  27495  noextendseq  27635  oldf  27833  leftssno  27869  rightssno  27870  addbdaylem  28013  mulsproplem12  28123  mulsproplem13  28124  mulsproplem14  28125  mulsasslem3  28161  precsexlem11  28213  oncutlt  28260  bdayons  28272  nnssno  28318  axtgcgrrflx  28534  axtgcgrid  28535  axtgsegcon  28536  axtg5seg  28537  axtgbtwnid  28538  axtgpasch  28539  axtgcont1  28540  tgcgr4  28603  motcgrg  28616  tglng  28618  upgrss  29161  pthdivtx  29800  disjxwwlkn  29986  ex-fpar  30537  nmlno0lem  30868  hlimcaui  31311  chsspwh  31322  shsss  31388  chintcli  31406  shsleji  31445  shub1i  31449  shsval2i  31462  lejdii  31613  spanuni  31619  sshhococi  31621  spansnpji  31653  osumcori  31718  5oai  31736  3oalem6  31742  3oai  31743  pjssmii  31756  mayete3i  31803  mayetes3i  31804  nmlnop0iALT  32070  imaelshi  32133  pjnmopi  32223  pjclem1  32270  pjci  32275  mdslmd1lem1  32400  shatomistici  32436  hatomistici  32437  chpssati  32438  xppreima  32723  iundisjfi  32876  iundisj2fi  32877  fprodex01  32906  indsumin  32943  xrsmulgzz  33091  fsumrp0cl  33103  gsummpt2co  33131  cycpmfv2  33196  cycpmrn  33225  rlocbas  33349  rlocaddval  33350  rlocmulval  33351  1fldgenq  33404  xrge0slmod  33429  lsmsnorb  33472  idlsrgbas  33585  idlsrgplusg  33586  idlsrgmulr  33588  idlsrgtset  33589  esplyind  33731  vietalem  33735  constrextdg2  33906  ordtconnlem1  34081  xrge0iifhom  34094  lmlimxrge0  34105  lmxrge0  34109  esumcst  34220  esumpfinvallem  34231  esumpfinval  34232  esumpfinvalf  34233  esumcvg  34243  imambfm  34419  elmbfmvol2  34424  sxbrsigalem3  34429  sxbrsigalem2  34443  sxbrsigalem4  34444  sitgclg  34499  eulerpartlem1  34524  eulerpartlemgvv  34533  eulerpartlemgh  34535  eulerpartlemgf  34536  ballotlemfc0  34650  ballotlemfcc  34651  ballotlemiex  34659  ballotlemsup  34662  ballotlemsima  34673  ballotlemrv2  34679  ballotth  34695  signsplypnf  34707  signsply0  34708  rpsqrtcn  34750  itgexpif  34763  fsum2dsub  34764  reprfi2  34780  chtvalz  34786  breprexplemc  34789  breprexpnat  34791  circlemeth  34797  circlemethnat  34798  circlevma  34799  circlemethhgt  34800  hgt750lemd  34805  hgt750lema  34814  tgoldbachgtde  34817  tgoldbachgtda  34818  tgoldbachgt  34820  bnj1145  35149  bnj1286  35175  subfacp1lem2a  35374  erdszelem4  35388  erdszelem5  35389  erdszelem7  35391  erdszelem8  35392  kur14lem7  35406  kur14lem9  35408  resconn  35440  iccllysconn  35444  txpss3v  36070  txprel  36071  limitssson  36103  finminlem  36512  tailf  36569  filnetlem3  36574  onint1  36643  bj-unrab  37127  bj-2upln1upl  37225  bj-imdirco  37391  bj-rvecssabl  37507  taupilem2  37523  taupi  37524  poimirlem3  37820  poimirlem30  37847  poimirlem31  37848  poimirlem32  37849  broucube  37851  opnmbllem0  37853  mblfinlem1  37854  mblfinlem2  37855  mblfinlem3  37856  mblfinlem4  37857  ismblfin  37858  mbfposadd  37864  cnambfre  37865  itg2addnc  37871  ftc1cnnclem  37888  ftc1cnnc  37889  ftc1anclem3  37892  ftc1anclem7  37896  ftc1anc  37898  ftc2nc  37899  dvreasin  37903  dvreacos  37904  areacirclem1  37905  areacirclem2  37906  areacirc  37910  caures  37957  reheibor  38036  xrnss3v  38562  xrnrel  38563  atlatmstc  39575  atlatle  39576  pmaple  40017  sspadd1  40071  sspadd2  40072  dvrelog2  42314  dvrelog3  42315  rpsscn  42550  sumcubes  42564  redvmptabs  42611  diophin  43010  4rexfrabdioph  43036  6rexfrabdioph  43037  irrapxlem1  43060  irrapx1  43066  rmxyelqirr  43148  monotuz  43179  jm2.27dlem5  43251  hbtlem2  43362  algbase  43412  algaddg  43413  algmulr  43414  algsca  43415  algvsca  43416  arearect  43453  areaquad  43454  rtrclex  43854  trclubgNEW  43855  trclexi  43857  rtrclexi  43858  cnvtrcl0  43863  dfrtrcl5  43866  trrelsuperrel2dg  43908  relexpaddss  43955  brtrclfv2  43964  frege131d  44001  xphe  44018  clsk3nimkb  44277  gneispace  44371  k0004val0  44391  inaex  44534  lhe4.4ex1a  44566  uzmptshftfval  44583  binomcxplemdvbinom  44590  binomcxplemcvg  44591  binomcxplemnotnn0  44593  relopabVD  45137  dmwf  45202  rnwf  45203  fzisoeu  45544  fzsscn  45555  fzssre  45558  fzossuz  45621  zssxr  45637  uzssre2  45647  supminfxr  45704  uzsscn  45715  rpssxr  45720  uzinico  45801  limcresiooub  45882  limcresioolb  45883  limcleqr  45884  limclner  45891  limclr  45895  limsupequzmpt2  45958  liminfval2  46008  liminfequzmpt2  46031  icccncfext  46127  cncficcgt0  46128  ioodvbdlimc1lem2  46172  ioodvbdlimc2lem  46174  dvnprodlem2  46187  itgsin0pilem1  46190  itgsinexplem1  46194  itgsinexp  46195  dirkercncflem2  46344  fourierdlem16  46363  fourierdlem18  46365  fourierdlem20  46367  fourierdlem21  46368  fourierdlem22  46369  fourierdlem25  46372  fourierdlem37  46384  fourierdlem42  46389  fourierdlem50  46396  fourierdlem52  46398  fourierdlem62  46408  fourierdlem64  46410  fourierdlem66  46412  fourierdlem68  46414  fourierdlem74  46420  fourierdlem75  46421  fourierdlem76  46422  fourierdlem79  46425  fourierdlem83  46429  fourierdlem95  46441  fourierdlem101  46447  fourierdlem102  46448  fourierdlem103  46449  fourierdlem104  46450  fourierdlem112  46458  fourierdlem114  46460  sqwvfoura  46468  sqwvfourb  46469  fouriersw  46471  etransclem24  46498  etransclem48  46522  sge0sn  46619  sge0tsms  46620  sge0f1o  46622  sge0pr  46634  sge0resplit  46646  sge0split  46649  sge0iunmptlemre  46655  sge0isummpt2  46672  carageniuncllem1  46761  hoicvr  46788  hoicvrrex  46796  hoidmvlelem2  46836  hspmbl  46869  smfmullem4  47034  chnsuslle  47121  lamberte  47130  rehalfge1  47577  prmdvdsfmtnof1lem1  47826  prmdvdsfmtnof  47828  upgrimpthslem2  48150  upgrimpths  48151  oddibas  48415  2zrngbas  48484  2zrng0  48486  dmtposss  49117  tposres3  49122  sepfsepc  49169  uptrlem1  49451  uptrlem2  49452  uptrlem3  49453  uptra  49456  uptrar  49457  uobeqw  49460  uptr2  49462  uptr2a  49463  fucoppcfunc  49653  aacllem  50042  amgmlemALT  50044