Theorem sstri 3953

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

Syntax hints:   ⊆ wss 3911

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

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

This theorem is referenced by:  snsstp1  4776  snsstp2  4777  uniintsn  4945  elopabran  5516  ssrnres  6139  cossxp  6233  foimacnv  6799  ssimaex  6928  riotassuni  7366  oprabss  7477  dmexg  7857  rnexg  7858  fabexgOLD  7895  mptmpoopabbrd  8038  fparlem3  8070  fparlem4  8071  snopsuppss  8135  tposssxp  8186  naddunif  8634  naddasslem1  8635  naddasslem2  8636  mapsspw  8828  sbthlem5  9032  sbthlem7  9034  cnvimamptfin  9280  marypha1lem  9360  ordtypelem4  9450  hartogslem1  9471  ttrclco  9647  cottrcl  9648  tc2  9671  frmin  9678  frrlem16  9687  tz9.12lem1  9716  rankval4  9796  rankxpl  9804  rankmapu  9807  rankxplim  9808  djuin  9847  infxpenlem  9942  ackbij1lem18  10165  cflm  10179  fin23lem29  10270  hsmexlem4  10358  hsmexlem5  10359  brdom3  10457  brdom5  10458  brdom4  10459  smobeth  10515  pwfseqlem3  10589  wundm  10657  wunrn  10658  wunex2  10667  ltsopi  10817  dmaddpi  10819  dmmulpi  10820  nqerf  10859  ltrelxr  11211  uzssre  12791  uzwo2  12847  infssuzle  12866  infssuzcl  12867  uzwo3  12878  nn0ssq  12892  nnssq  12893  qsscn  12895  rpnnen1lem3  12914  rpnnen1lem5  12916  dflt2  13084  ioosscn  13345  unitsscn  13437  fzval2  13447  fzossz  13616  fzossnn  13648  injresinj  13725  flval3  13753  uzsup  13801  uzrdgfni  13899  expcl2lem  14014  rpexpcl  14021  expge0  14039  expge1  14040  hashxrcl  14298  seqcoll  14405  xptrrel  14922  trclublem  14937  01sqrexlem3  15186  limsupval2  15422  limsupgre  15423  rlimpm  15442  rlimclim  15488  isercolllem1  15607  isercolllem2  15608  isercoll  15610  caurcvg  15619  caucvg  15621  summolem2a  15657  summolem2  15658  zsum  15660  fsumcvg3  15671  fsumrpcl  15679  fsumge0  15737  climfsum  15762  ackbijnn  15770  prodmolem2a  15876  prodmolem2  15877  zprod  15879  fprodrpcl  15898  fprodge0  15935  fprodge1  15937  rprisefaccl  15965  divalglem8  16346  sadaddlem  16412  lcmfval  16567  isprm3  16629  maxprmfct  16655  pclem  16785  prmreclem1  16863  prmreclem2  16864  prmreclem3  16865  1arith  16874  4sqlem11  16902  ramtlecl  16947  ramcl2lem  16956  ramxrcl  16964  prmgaplem3  17000  prmgaplem4  17001  cshwshashlem1  17042  structfn  17102  strleun  17103  ressbasss  17185  ressbasss2  17187  srngbase  17249  srngplusg  17250  srngmulr  17251  lmodbase  17265  lmodplusg  17266  lmodsca  17267  ipsbase  17276  ipsaddg  17277  ipsmulr  17278  ipssca  17279  ipsvsca  17280  ipsip  17281  phlbase  17286  phlplusg  17287  phlsca  17288  phlvsca  17289  phlip  17290  odrngbas  17343  odrngplusg  17344  odrngmulr  17345  odrngtset  17346  odrngle  17347  odrngds  17348  prdsvallem  17393  prdsval  17394  prdssca  17395  prdsbas  17396  prdsplusg  17397  prdsmulr  17398  prdsvsca  17399  prdsip  17400  prdsle  17401  prdsds  17403  prdstset  17405  prdshom  17406  prdsco  17407  imasbas  17451  imasds  17452  imasplusg  17456  imasmulr  17457  imassca  17458  imasvsca  17459  imasip  17460  imastset  17461  imasle  17462  wunfunc  17839  fullfunc  17846  fthfunc  17847  isfull  17850  isfth  17854  wunnat  17897  dmcoass  18004  catcisolem  18048  catciso  18049  catcoppccl  18055  catcfuccl  18056  catcxpccl  18144  ipobas  18466  ipolerval  18467  ipotset  18468  psdmrn  18508  psss  18515  ledm  18525  lern  18526  dirdm  18535  dirge  18538  mulgfval  18977  mvdco  19351  f1omvdconj  19352  gexex  19759  gsumval3  19813  lssacs  20849  cnfldbas  21244  mpocnfldadd  21245  mpocnfldmul  21247  cnfldcj  21249  cnfldtset  21250  cnfldle  21251  cnfldds  21252  cnfldunif  21253  cnfldbasOLD  21259  cnfldaddOLD  21260  cnfldmulOLD  21261  cnfldcjOLD  21262  cnfldtsetOLD  21263  cnfldleOLD  21264  cnflddsOLD  21265  cnfldunifOLD  21266  rge0srg  21331  zntoslem  21442  asplss  21759  aspsubrg  21761  psrass1lem  21817  psrbas  21818  psrplusg  21821  psrmulr  21827  psrsca  21832  psrvscafval  21833  psrass1  21849  psrass23l  21852  psrcom  21853  psrass23  21854  psropprmul  22098  coe1mul2  22131  ofco2  22314  toponsspwpw  22785  dmtopon  22786  leordtval2  23075  lmbrf  23123  lmres  23163  fiuncmp  23267  comppfsc  23395  1stckgenlem  23416  kgencn3  23421  ptbasfi  23444  xkoopn  23452  txcnmpt  23487  txkgen  23515  opnfbas  23705  fmfnfmlem4  23820  tsmsxplem1  24016  trust  24093  restutop  24101  nmoffn  24575  nmofval  24578  nmogelb  24580  nmolb  24581  nmof  24583  qtopbas  24623  tgqioo  24664  re2ndc  24665  iitopon  24748  dfii3  24752  iimulcnOLD  24811  cnheiborlem  24829  bndth  24833  lebnumii  24841  reparphtiOLD  24873  pcoass  24900  cphsqrtcl  25060  lmmbrf  25138  iscauf  25156  caucfil  25159  lmclimf  25180  rrxmval  25281  rrxmet  25284  ovolfioo  25344  ovolficc  25345  ovolficcss  25346  ovolfsf  25348  ovollb  25356  ovolicc2lem3  25396  ovolicc2lem4  25397  ovolicc2  25399  volf  25406  volsup  25433  ovolfs2  25448  uniiccdif  25455  uniioovol  25456  uniiccvol  25457  uniioombllem2  25460  uniioombllem3a  25461  uniioombllem3  25462  uniioombllem4  25463  uniioombllem5  25464  uniioombl  25466  dyadmbllem  25476  dyadmbl  25477  opnmbllem  25478  opnmblALT  25480  volsup2  25482  vitalilem4  25488  vitalilem5  25489  vitali  25490  mbfimaopnlem  25532  mbflimsup  25543  i1f0  25564  i1f1  25567  itg11  25568  itg2mulc  25624  itg2gt0  25637  ellimc2  25754  limcresi  25762  dvreslem  25786  dvres2lem  25787  dvaddbr  25816  dvmulbr  25817  dvmulbrOLD  25818  dvlipcn  25875  c1liplem1  25877  lhop1lem  25894  lhop1  25895  lhop2  25896  lhop  25897  dvfsumrlim  25914  ftc1cn  25926  itgsubstlem  25931  itgsubst  25932  itgpowd  25933  mdegleb  25945  mdeglt  25946  mdegldg  25947  mdegxrcl  25948  mdegcl  25950  mdegaddle  25955  mdegmullem  25959  deg1mul3le  25998  ig1peu  26056  ig1pdvds  26061  aacjcl  26211  aannenlem2  26213  aannenlem3  26214  aalioulem2  26217  taylfval  26242  radcnvcl  26302  radcnvlt1  26303  radcnvle  26305  abelth  26327  abelth2  26328  pilem2  26338  pilem3  26339  pige3ALT  26405  recosf1o  26420  resinf1o  26421  tanord1  26422  logcn  26532  dvlog  26536  dvlog2lem  26537  efopn  26543  logtayl  26545  cxpcn3  26634  loglesqrt  26647  ssscongptld  26708  leibpi  26828  efrlim  26855  efrlimOLD  26856  jensenlem1  26873  jensenlem2  26874  jensen  26875  amgm  26877  lgamgulmlem2  26916  ftalem5  26963  efnnfsumcl  26989  efchtdvds  27045  mpodvdsmulf1o  27080  fsumdvdsmul  27081  dvdsmulf1o  27082  fsumdvdsmulOLD  27083  lgsfcl2  27190  2sqlem6  27310  2sqlem8  27313  2sqlem9  27314  rpvmasumlem  27374  rpvmasum2  27399  dchrisum0re  27400  dchrisum0lem3  27406  dchrisum0  27407  rplogsum  27414  dirith2  27415  noextendseq  27555  oldf  27741  leftssno  27768  rightssno  27769  addsbdaylem  27899  mulsproplem12  28006  mulsproplem13  28007  mulsproplem14  28008  mulsasslem3  28044  precsexlem11  28095  onscutlt  28141  bdayon  28149  nnssno  28191  axtgcgrrflx  28365  axtgcgrid  28366  axtgsegcon  28367  axtg5seg  28368  axtgbtwnid  28369  axtgpasch  28370  axtgcont1  28371  tgcgr4  28434  motcgrg  28447  tglng  28449  upgrss  28991  pthdivtx  29630  disjxwwlkn  29816  ex-fpar  30364  nmlno0lem  30695  hlimcaui  31138  chsspwh  31149  shsss  31215  chintcli  31233  shsleji  31272  shub1i  31276  shsval2i  31289  lejdii  31440  spanuni  31446  sshhococi  31448  spansnpji  31480  osumcori  31545  5oai  31563  3oalem6  31569  3oai  31570  pjssmii  31583  mayete3i  31630  mayetes3i  31631  nmlnop0iALT  31897  imaelshi  31960  pjnmopi  32050  pjclem1  32097  pjci  32102  mdslmd1lem1  32227  shatomistici  32263  hatomistici  32264  chpssati  32265  xppreima  32542  iundisjfi  32692  iundisj2fi  32693  fprodex01  32723  indsumin  32758  xrsmulgzz  32920  fsumrp0cl  32935  gsummpt2co  32961  cycpmfv2  33044  cycpmrn  33073  rlocbas  33191  rlocaddval  33192  rlocmulval  33193  1fldgenq  33245  xrge0slmod  33292  lsmsnorb  33335  idlsrgbas  33448  idlsrgplusg  33449  idlsrgmulr  33451  idlsrgtset  33452  constrextdg2  33712  ordtconnlem1  33887  xrge0iifhom  33900  lmlimxrge0  33911  lmxrge0  33915  esumcst  34026  esumpfinvallem  34037  esumpfinval  34038  esumpfinvalf  34039  esumcvg  34049  imambfm  34226  elmbfmvol2  34231  sxbrsigalem3  34236  sxbrsigalem2  34250  sxbrsigalem4  34251  sitgclg  34306  eulerpartlem1  34331  eulerpartlemgvv  34340  eulerpartlemgh  34342  eulerpartlemgf  34343  ballotlemfc0  34457  ballotlemfcc  34458  ballotlemiex  34466  ballotlemsup  34469  ballotlemsima  34480  ballotlemrv2  34486  ballotth  34502  signsplypnf  34514  signsply0  34515  rpsqrtcn  34557  itgexpif  34570  fsum2dsub  34571  reprfi2  34587  chtvalz  34593  breprexplemc  34596  breprexpnat  34598  circlemeth  34604  circlemethnat  34605  circlevma  34606  circlemethhgt  34607  hgt750lemd  34612  hgt750lema  34621  tgoldbachgtde  34624  tgoldbachgtda  34625  tgoldbachgt  34627  bnj1145  34956  bnj1286  34982  subfacp1lem2a  35140  erdszelem4  35154  erdszelem5  35155  erdszelem7  35157  erdszelem8  35158  kur14lem7  35172  kur14lem9  35174  resconn  35206  iccllysconn  35210  txpss3v  35839  txprel  35840  limitssson  35872  finminlem  36279  tailf  36336  filnetlem3  36341  onint1  36410  bj-unrab  36887  bj-2upln1upl  36985  bj-imdirco  37151  bj-rvecssabl  37267  taupilem2  37283  taupi  37284  poimirlem3  37590  poimirlem30  37617  poimirlem31  37618  poimirlem32  37619  broucube  37621  opnmbllem0  37623  mblfinlem1  37624  mblfinlem2  37625  mblfinlem3  37626  mblfinlem4  37627  ismblfin  37628  mbfposadd  37634  cnambfre  37635  itg2addnc  37641  ftc1cnnclem  37658  ftc1cnnc  37659  ftc1anclem3  37662  ftc1anclem7  37666  ftc1anc  37668  ftc2nc  37669  dvreasin  37673  dvreacos  37674  areacirclem1  37675  areacirclem2  37676  areacirc  37680  caures  37727  reheibor  37806  xrnss3v  38327  xrnrel  38328  atlatmstc  39285  atlatle  39286  pmaple  39728  sspadd1  39782  sspadd2  39783  dvrelog2  42025  dvrelog3  42026  rpsscn  42260  sumcubes  42274  redvmptabs  42321  diophin  42733  4rexfrabdioph  42759  6rexfrabdioph  42760  irrapxlem1  42783  irrapx1  42789  rmxyelqirr  42871  monotuz  42903  jm2.27dlem5  42975  hbtlem2  43086  algbase  43136  algaddg  43137  algmulr  43138  algsca  43139  algvsca  43140  arearect  43177  areaquad  43178  rtrclex  43579  trclubgNEW  43580  trclexi  43582  rtrclexi  43583  cnvtrcl0  43588  dfrtrcl5  43591  trrelsuperrel2dg  43633  relexpaddss  43680  brtrclfv2  43689  frege131d  43726  xphe  43743  clsk3nimkb  44002  gneispace  44096  k0004val0  44116  inaex  44259  lhe4.4ex1a  44291  uzmptshftfval  44308  binomcxplemdvbinom  44315  binomcxplemcvg  44316  binomcxplemnotnn0  44318  relopabVD  44863  dmwf  44928  rnwf  44929  fzisoeu  45271  fzsscn  45282  fzssre  45285  fzossuz  45350  zssxr  45366  uzssre2  45376  supminfxr  45433  uzsscn  45444  rpssxr  45449  uzinico  45530  limcresiooub  45613  limcresioolb  45614  limcleqr  45615  limclner  45622  limclr  45626  limsupequzmpt2  45689  liminfval2  45739  liminfequzmpt2  45762  icccncfext  45858  cncficcgt0  45859  ioodvbdlimc1lem2  45903  ioodvbdlimc2lem  45905  dvnprodlem2  45918  itgsin0pilem1  45921  itgsinexplem1  45925  itgsinexp  45926  dirkercncflem2  46075  fourierdlem16  46094  fourierdlem18  46096  fourierdlem20  46098  fourierdlem21  46099  fourierdlem22  46100  fourierdlem25  46103  fourierdlem37  46115  fourierdlem42  46120  fourierdlem50  46127  fourierdlem52  46129  fourierdlem62  46139  fourierdlem64  46141  fourierdlem66  46143  fourierdlem68  46145  fourierdlem74  46151  fourierdlem75  46152  fourierdlem76  46153  fourierdlem79  46156  fourierdlem83  46160  fourierdlem95  46172  fourierdlem101  46178  fourierdlem102  46179  fourierdlem103  46180  fourierdlem104  46181  fourierdlem112  46189  fourierdlem114  46191  sqwvfoura  46199  sqwvfourb  46200  fouriersw  46202  etransclem24  46229  etransclem48  46253  sge0sn  46350  sge0tsms  46351  sge0f1o  46353  sge0pr  46365  sge0resplit  46377  sge0split  46380  sge0iunmptlemre  46386  sge0isummpt2  46403  carageniuncllem1  46492  hoicvr  46519  hoicvrrex  46527  hoidmvlelem2  46567  hspmbl  46600  smfmullem4  46765  lamberte  46862  rehalfge1  47309  prmdvdsfmtnof1lem1  47558  prmdvdsfmtnof  47560  upgrimpthslem2  47881  upgrimpths  47882  oddibas  48134  2zrngbas  48203  2zrng0  48205  dmtposss  48837  tposres3  48842  sepfsepc  48889  uptrlem1  49172  uptrlem2  49173  uptrlem3  49174  uptra  49177  uptrar  49178  uobeqw  49181  uptr2  49183  uptr2a  49184  fucoppcfunc  49374  aacllem  49763  amgmlemALT  49765