Theorem sstri 3932

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 3929	. 2 ⊢ (𝐴 ⊆ 𝐵 → (𝐵 ⊆ 𝐶 → 𝐴 ⊆ 𝐶))
4	1, 2, 3	mp2 9	1 ⊢ 𝐴 ⊆ 𝐶

Syntax hints:   ⊆ wss 3890

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

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

This theorem is referenced by:  snsstp1  4760  snsstp2  4761  uniintsn  4928  elopabran  5509  ssrnres  6136  cossxp  6230  foimacnv  6791  ssimaex  6919  riotassuni  7357  oprabss  7468  dmexg  7845  rnexg  7846  fabexgOLD  7883  mptmpoopabbrd  8026  fparlem3  8057  fparlem4  8058  snopsuppss  8122  tposssxp  8173  naddunif  8622  naddasslem1  8623  naddasslem2  8624  mapsspw  8819  sbthlem5  9022  sbthlem7  9024  cnvimamptfin  9256  marypha1lem  9339  ordtypelem4  9429  hartogslem1  9450  ttrclco  9630  cottrcl  9631  tc2  9652  frmin  9664  frrlem16  9673  tz9.12lem1  9702  rankval4  9782  rankxpl  9790  rankmapu  9793  rankxplim  9794  djuin  9833  infxpenlem  9926  ackbij1lem18  10149  cflm  10163  fin23lem29  10254  hsmexlem4  10342  hsmexlem5  10343  brdom3  10441  brdom5  10442  brdom4  10443  smobeth  10500  pwfseqlem3  10574  wundm  10642  wunrn  10643  wunex2  10652  ltsopi  10802  dmaddpi  10804  dmmulpi  10805  nqerf  10844  ltrelxr  11197  uzssre  12801  uzwo2  12853  infssuzle  12872  infssuzcl  12873  uzwo3  12884  nn0ssq  12898  nnssq  12899  qsscn  12901  rpnnen1lem3  12920  rpnnen1lem5  12922  dflt2  13090  ioosscn  13352  unitsscn  13444  fzval2  13455  fzossz  13625  fzossnn  13657  injresinj  13737  flval3  13765  uzsup  13813  uzrdgfni  13911  expcl2lem  14026  rpexpcl  14033  expge0  14051  expge1  14052  hashxrcl  14310  seqcoll  14417  xptrrel  14933  trclublem  14948  01sqrexlem3  15197  limsupval2  15433  limsupgre  15434  rlimpm  15453  rlimclim  15499  isercolllem1  15618  isercolllem2  15619  isercoll  15621  caurcvg  15630  caucvg  15632  summolem2a  15668  summolem2  15669  zsum  15671  fsumcvg3  15682  fsumrpcl  15690  fsumge0  15749  climfsum  15774  ackbijnn  15784  prodmolem2a  15890  prodmolem2  15891  zprod  15893  fprodrpcl  15912  fprodge0  15949  fprodge1  15951  rprisefaccl  15979  divalglem8  16360  sadaddlem  16426  lcmfval  16581  isprm3  16643  maxprmfct  16670  pclem  16800  prmreclem1  16878  prmreclem2  16879  prmreclem3  16880  1arith  16889  4sqlem11  16917  ramtlecl  16962  ramcl2lem  16971  ramxrcl  16979  prmgaplem3  17015  prmgaplem4  17016  cshwshashlem1  17057  structfn  17117  strleun  17118  ressbasss  17200  ressbasss2  17202  srngbase  17264  srngplusg  17265  srngmulr  17266  lmodbase  17280  lmodplusg  17281  lmodsca  17282  ipsbase  17291  ipsaddg  17292  ipsmulr  17293  ipssca  17294  ipsvsca  17295  ipsip  17296  phlbase  17301  phlplusg  17302  phlsca  17303  phlvsca  17304  phlip  17305  odrngbas  17358  odrngplusg  17359  odrngmulr  17360  odrngtset  17361  odrngle  17362  odrngds  17363  prdsvallem  17408  prdsval  17409  prdssca  17410  prdsbas  17411  prdsplusg  17412  prdsmulr  17413  prdsvsca  17414  prdsip  17415  prdsle  17416  prdsds  17418  prdstset  17420  prdshom  17421  prdsco  17422  imasbas  17467  imasds  17468  imasplusg  17472  imasmulr  17473  imassca  17474  imasvsca  17475  imasip  17476  imastset  17477  imasle  17478  wunfunc  17859  fullfunc  17866  fthfunc  17867  isfull  17870  isfth  17874  wunnat  17917  dmcoass  18024  catcisolem  18068  catciso  18069  catcoppccl  18075  catcfuccl  18076  catcxpccl  18164  ipobas  18488  ipolerval  18489  ipotset  18490  psdmrn  18530  psss  18537  ledm  18547  lern  18548  dirdm  18557  dirge  18560  mulgfval  19036  mvdco  19411  f1omvdconj  19412  gexex  19819  gsumval3  19873  lssacs  20953  cnfldbas  21348  mpocnfldadd  21349  mpocnfldmul  21351  cnfldcj  21353  cnfldtset  21354  cnfldle  21355  cnfldds  21356  cnfldunif  21357  cnfldbasOLD  21363  cnfldaddOLD  21364  cnfldmulOLD  21365  cnfldcjOLD  21366  cnfldtsetOLD  21367  cnfldleOLD  21368  cnflddsOLD  21369  cnfldunifOLD  21370  rge0srg  21428  zntoslem  21546  asplss  21863  aspsubrg  21865  psrass1lem  21922  psrbas  21923  psrplusg  21926  psrmulr  21931  psrsca  21936  psrvscafval  21937  psrass1  21952  psrass23l  21955  psrcom  21956  psrass23  21957  psropprmul  22211  coe1mul2  22244  ofco2  22426  toponsspwpw  22897  dmtopon  22898  leordtval2  23187  lmbrf  23235  lmres  23275  fiuncmp  23379  comppfsc  23507  1stckgenlem  23528  kgencn3  23533  ptbasfi  23556  xkoopn  23564  txcnmpt  23599  txkgen  23627  opnfbas  23817  fmfnfmlem4  23932  tsmsxplem1  24128  trust  24204  restutop  24212  nmoffn  24686  nmofval  24689  nmogelb  24691  nmolb  24692  nmof  24694  qtopbas  24734  tgqioo  24775  re2ndc  24776  iitopon  24856  dfii3  24860  cnheiborlem  24931  bndth  24935  lebnumii  24943  pcoass  25001  cphsqrtcl  25161  lmmbrf  25239  iscauf  25257  caucfil  25260  lmclimf  25281  rrxmval  25382  rrxmet  25385  ovolfioo  25444  ovolficc  25445  ovolficcss  25446  ovolfsf  25448  ovollb  25456  ovolicc2lem3  25496  ovolicc2lem4  25497  ovolicc2  25499  volf  25506  volsup  25533  ovolfs2  25548  uniiccdif  25555  uniioovol  25556  uniiccvol  25557  uniioombllem2  25560  uniioombllem3a  25561  uniioombllem3  25562  uniioombllem4  25563  uniioombllem5  25564  uniioombl  25566  dyadmbllem  25576  dyadmbl  25577  opnmbllem  25578  opnmblALT  25580  volsup2  25582  vitalilem4  25588  vitalilem5  25589  vitali  25590  mbfimaopnlem  25632  mbflimsup  25643  i1f0  25664  i1f1  25667  itg11  25668  itg2mulc  25724  itg2gt0  25737  ellimc2  25854  limcresi  25862  dvreslem  25886  dvres2lem  25887  dvaddbr  25915  dvmulbr  25916  dvlipcn  25971  c1liplem1  25973  lhop1lem  25990  lhop1  25991  lhop2  25992  lhop  25993  dvfsumrlim  26008  ftc1cn  26020  itgsubstlem  26025  itgsubst  26026  itgpowd  26027  mdegleb  26039  mdeglt  26040  mdegldg  26041  mdegxrcl  26042  mdegcl  26044  mdegaddle  26049  mdegmullem  26053  deg1mul3le  26092  ig1peu  26150  ig1pdvds  26155  aacjcl  26304  aannenlem2  26306  aannenlem3  26307  aalioulem2  26310  taylfval  26335  radcnvcl  26395  radcnvlt1  26396  radcnvle  26398  abelth  26419  abelth2  26420  pilem2  26430  pilem3  26431  pige3ALT  26497  recosf1o  26512  resinf1o  26513  tanord1  26514  logcn  26624  dvlog  26628  dvlog2lem  26629  efopn  26635  logtayl  26637  cxpcn3  26725  loglesqrt  26738  ssscongptld  26799  leibpi  26919  efrlim  26946  efrlimOLD  26947  jensenlem1  26964  jensenlem2  26965  jensen  26966  amgm  26968  lgamgulmlem2  27007  ftalem5  27054  efnnfsumcl  27080  efchtdvds  27136  mpodvdsmulf1o  27171  fsumdvdsmul  27172  dvdsmulf1o  27173  lgsfcl2  27280  2sqlem6  27400  2sqlem8  27403  2sqlem9  27404  rpvmasumlem  27464  rpvmasum2  27489  dchrisum0re  27490  dchrisum0lem3  27496  dchrisum0  27497  rplogsum  27504  dirith2  27505  noextendseq  27645  oldf  27843  leftssno  27879  rightssno  27880  addbdaylem  28023  mulsproplem12  28133  mulsproplem13  28134  mulsproplem14  28135  mulsasslem3  28171  precsexlem11  28223  oncutlt  28270  bdayons  28282  nnssno  28328  axtgcgrrflx  28544  axtgcgrid  28545  axtgsegcon  28546  axtg5seg  28547  axtgbtwnid  28548  axtgpasch  28549  axtgcont1  28550  tgcgr4  28613  motcgrg  28626  tglng  28628  upgrss  29171  pthdivtx  29810  disjxwwlkn  29996  ex-fpar  30547  nmlno0lem  30879  hlimcaui  31322  chsspwh  31333  shsss  31399  chintcli  31417  shsleji  31456  shub1i  31460  shsval2i  31473  lejdii  31624  spanuni  31630  sshhococi  31632  spansnpji  31664  osumcori  31729  5oai  31747  3oalem6  31753  3oai  31754  pjssmii  31767  mayete3i  31814  mayetes3i  31815  nmlnop0iALT  32081  imaelshi  32144  pjnmopi  32234  pjclem1  32281  pjci  32286  mdslmd1lem1  32411  shatomistici  32447  hatomistici  32448  chpssati  32449  xppreima  32733  iundisjfi  32884  iundisj2fi  32885  fprodex01  32913  indsumin  32936  xrsmulgzz  33084  fsumrp0cl  33096  gsummpt2co  33124  cycpmfv2  33190  cycpmrn  33219  rlocbas  33343  rlocaddval  33344  rlocmulval  33345  1fldgenq  33398  xrge0slmod  33423  lsmsnorb  33466  idlsrgbas  33579  idlsrgplusg  33580  idlsrgmulr  33582  idlsrgtset  33583  esplyind  33734  vietalem  33738  constrextdg2  33909  ordtconnlem1  34084  xrge0iifhom  34097  lmlimxrge0  34108  lmxrge0  34112  esumcst  34223  esumpfinvallem  34234  esumpfinval  34235  esumpfinvalf  34236  esumcvg  34246  imambfm  34422  elmbfmvol2  34427  sxbrsigalem3  34432  sxbrsigalem2  34446  sxbrsigalem4  34447  sitgclg  34502  eulerpartlem1  34527  eulerpartlemgvv  34536  eulerpartlemgh  34538  eulerpartlemgf  34539  ballotlemfc0  34653  ballotlemfcc  34654  ballotlemiex  34662  ballotlemsup  34665  ballotlemsima  34676  ballotlemrv2  34682  ballotth  34698  signsplypnf  34710  signsply0  34711  rpsqrtcn  34753  itgexpif  34766  fsum2dsub  34767  reprfi2  34783  chtvalz  34789  breprexplemc  34792  breprexpnat  34794  circlemeth  34800  circlemethnat  34801  circlevma  34802  circlemethhgt  34803  hgt750lemd  34808  hgt750lema  34817  tgoldbachgtde  34820  tgoldbachgtda  34821  tgoldbachgt  34823  bnj1145  35151  bnj1286  35177  subfacp1lem2a  35378  erdszelem4  35392  erdszelem5  35393  erdszelem7  35395  erdszelem8  35396  kur14lem7  35410  kur14lem9  35412  resconn  35444  iccllysconn  35448  txpss3v  36074  txprel  36075  limitssson  36107  finminlem  36516  tailf  36573  filnetlem3  36578  onint1  36647  ttcuniun  36708  bj-unrab  37249  bj-2upln1upl  37347  bj-imdirco  37520  bj-rvecssabl  37636  taupilem2  37652  taupi  37653  poimirlem3  37958  poimirlem30  37985  poimirlem31  37986  poimirlem32  37987  broucube  37989  opnmbllem0  37991  mblfinlem1  37992  mblfinlem2  37993  mblfinlem3  37994  mblfinlem4  37995  ismblfin  37996  mbfposadd  38002  cnambfre  38003  itg2addnc  38009  ftc1cnnclem  38026  ftc1cnnc  38027  ftc1anclem3  38030  ftc1anclem7  38034  ftc1anc  38036  ftc2nc  38037  dvreasin  38041  dvreacos  38042  areacirclem1  38043  areacirclem2  38044  areacirc  38048  caures  38095  reheibor  38174  xrnss3v  38716  xrnrel  38717  atlatmstc  39779  atlatle  39780  pmaple  40221  sspadd1  40275  sspadd2  40276  dvrelog2  42517  dvrelog3  42518  rpsscn  42745  sumcubes  42759  redvmptabs  42806  diophin  43218  4rexfrabdioph  43244  6rexfrabdioph  43245  irrapxlem1  43268  irrapx1  43274  rmxyelqirr  43356  monotuz  43387  jm2.27dlem5  43459  hbtlem2  43570  algbase  43620  algaddg  43621  algmulr  43622  algsca  43623  algvsca  43624  arearect  43661  areaquad  43662  rtrclex  44062  trclubgNEW  44063  trclexi  44065  rtrclexi  44066  cnvtrcl0  44071  dfrtrcl5  44074  trrelsuperrel2dg  44116  relexpaddss  44163  brtrclfv2  44172  frege131d  44209  xphe  44226  clsk3nimkb  44485  gneispace  44579  k0004val0  44599  inaex  44742  lhe4.4ex1a  44774  uzmptshftfval  44791  binomcxplemdvbinom  44798  binomcxplemcvg  44799  binomcxplemnotnn0  44801  relopabVD  45345  dmwf  45410  rnwf  45411  fzisoeu  45751  fzsscn  45762  fzssre  45765  fzossuz  45828  zssxr  45844  uzssre2  45853  supminfxr  45910  uzsscn  45921  rpssxr  45926  uzinico  46007  limcresiooub  46088  limcresioolb  46089  limcleqr  46090  limclner  46097  limclr  46101  limsupequzmpt2  46164  liminfval2  46214  liminfequzmpt2  46237  icccncfext  46333  cncficcgt0  46334  ioodvbdlimc1lem2  46378  ioodvbdlimc2lem  46380  dvnprodlem2  46393  itgsin0pilem1  46396  itgsinexplem1  46400  itgsinexp  46401  dirkercncflem2  46550  fourierdlem16  46569  fourierdlem18  46571  fourierdlem20  46573  fourierdlem21  46574  fourierdlem22  46575  fourierdlem25  46578  fourierdlem37  46590  fourierdlem42  46595  fourierdlem50  46602  fourierdlem52  46604  fourierdlem62  46614  fourierdlem64  46616  fourierdlem66  46618  fourierdlem68  46620  fourierdlem74  46626  fourierdlem75  46627  fourierdlem76  46628  fourierdlem79  46631  fourierdlem83  46635  fourierdlem95  46647  fourierdlem101  46653  fourierdlem102  46654  fourierdlem103  46655  fourierdlem104  46656  fourierdlem112  46664  fourierdlem114  46666  sqwvfoura  46674  sqwvfourb  46675  fouriersw  46677  etransclem24  46704  etransclem48  46728  sge0sn  46825  sge0tsms  46826  sge0f1o  46828  sge0pr  46840  sge0resplit  46852  sge0split  46855  sge0iunmptlemre  46861  sge0isummpt2  46878  carageniuncllem1  46967  hoicvr  46994  hoicvrrex  47002  hoidmvlelem2  47042  hspmbl  47075  smfmullem4  47240  chnsuslle  47327  lamberte  47348  rehalfge1  47799  prmdvdsfmtnof1lem1  48059  prmdvdsfmtnof  48061  upgrimpthslem2  48396  upgrimpths  48397  oddibas  48661  2zrngbas  48730  2zrng0  48732  dmtposss  49363  tposres3  49368  sepfsepc  49415  uptrlem1  49697  uptrlem2  49698  uptrlem3  49699  uptra  49702  uptrar  49703  uobeqw  49706  uptr2  49708  uptr2a  49709  fucoppcfunc  49899  aacllem  50288  amgmlemALT  50290