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  37395  bj-rvecssabl  37511  taupilem2  37527  taupi  37528  poimirlem3  37824  poimirlem30  37851  poimirlem31  37852  poimirlem32  37853  broucube  37855  opnmbllem0  37857  mblfinlem1  37858  mblfinlem2  37859  mblfinlem3  37860  mblfinlem4  37861  ismblfin  37862  mbfposadd  37868  cnambfre  37869  itg2addnc  37875  ftc1cnnclem  37892  ftc1cnnc  37893  ftc1anclem3  37896  ftc1anclem7  37900  ftc1anc  37902  ftc2nc  37903  dvreasin  37907  dvreacos  37908  areacirclem1  37909  areacirclem2  37910  areacirc  37914  caures  37961  reheibor  38040  xrnss3v  38566  xrnrel  38567  atlatmstc  39579  atlatle  39580  pmaple  40021  sspadd1  40075  sspadd2  40076  dvrelog2  42318  dvrelog3  42319  rpsscn  42554  sumcubes  42568  redvmptabs  42615  diophin  43014  4rexfrabdioph  43040  6rexfrabdioph  43041  irrapxlem1  43064  irrapx1  43070  rmxyelqirr  43152  monotuz  43183  jm2.27dlem5  43255  hbtlem2  43366  algbase  43416  algaddg  43417  algmulr  43418  algsca  43419  algvsca  43420  arearect  43457  areaquad  43458  rtrclex  43858  trclubgNEW  43859  trclexi  43861  rtrclexi  43862  cnvtrcl0  43867  dfrtrcl5  43870  trrelsuperrel2dg  43912  relexpaddss  43959  brtrclfv2  43968  frege131d  44005  xphe  44022  clsk3nimkb  44281  gneispace  44375  k0004val0  44395  inaex  44538  lhe4.4ex1a  44570  uzmptshftfval  44587  binomcxplemdvbinom  44594  binomcxplemcvg  44595  binomcxplemnotnn0  44597  relopabVD  45141  dmwf  45206  rnwf  45207  fzisoeu  45548  fzsscn  45559  fzssre  45562  fzossuz  45625  zssxr  45641  uzssre2  45651  supminfxr  45708  uzsscn  45719  rpssxr  45724  uzinico  45805  limcresiooub  45886  limcresioolb  45887  limcleqr  45888  limclner  45895  limclr  45899  limsupequzmpt2  45962  liminfval2  46012  liminfequzmpt2  46035  icccncfext  46131  cncficcgt0  46132  ioodvbdlimc1lem2  46176  ioodvbdlimc2lem  46178  dvnprodlem2  46191  itgsin0pilem1  46194  itgsinexplem1  46198  itgsinexp  46199  dirkercncflem2  46348  fourierdlem16  46367  fourierdlem18  46369  fourierdlem20  46371  fourierdlem21  46372  fourierdlem22  46373  fourierdlem25  46376  fourierdlem37  46388  fourierdlem42  46393  fourierdlem50  46400  fourierdlem52  46402  fourierdlem62  46412  fourierdlem64  46414  fourierdlem66  46416  fourierdlem68  46418  fourierdlem74  46424  fourierdlem75  46425  fourierdlem76  46426  fourierdlem79  46429  fourierdlem83  46433  fourierdlem95  46445  fourierdlem101  46451  fourierdlem102  46452  fourierdlem103  46453  fourierdlem104  46454  fourierdlem112  46462  fourierdlem114  46464  sqwvfoura  46472  sqwvfourb  46473  fouriersw  46475  etransclem24  46502  etransclem48  46526  sge0sn  46623  sge0tsms  46624  sge0f1o  46626  sge0pr  46638  sge0resplit  46650  sge0split  46653  sge0iunmptlemre  46659  sge0isummpt2  46676  carageniuncllem1  46765  hoicvr  46792  hoicvrrex  46800  hoidmvlelem2  46840  hspmbl  46873  smfmullem4  47038  chnsuslle  47125  lamberte  47134  rehalfge1  47581  prmdvdsfmtnof1lem1  47830  prmdvdsfmtnof  47832  upgrimpthslem2  48154  upgrimpths  48155  oddibas  48419  2zrngbas  48488  2zrng0  48490  dmtposss  49121  tposres3  49126  sepfsepc  49173  uptrlem1  49455  uptrlem2  49456  uptrlem3  49457  uptra  49460  uptrar  49461  uobeqw  49464  uptr2  49466  uptr2a  49467  fucoppcfunc  49657  aacllem  50046  amgmlemALT  50048