Theorem sstri 4018

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

Syntax hints:   ⊆ wss 3976

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

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

This theorem is referenced by:  snsstp1  4841  snsstp2  4842  uniintsn  5009  elopabran  5581  ssrnres  6209  cossxp  6303  foimacnv  6879  ssimaex  7007  riotassuni  7445  oprabss  7557  dmexg  7941  rnexg  7942  fabexgOLD  7977  mptmpoopabbrd  8121  fparlem3  8155  fparlem4  8156  snopsuppss  8220  tposssxp  8271  naddunif  8749  naddasslem1  8750  naddasslem2  8751  mapsspw  8936  sbthlem5  9153  sbthlem7  9155  cnvimamptfin  9423  marypha1lem  9502  ordtypelem4  9590  hartogslem1  9611  ttrclco  9787  cottrcl  9788  tc2  9811  frmin  9818  frrlem16  9827  tz9.12lem1  9856  rankval4  9936  rankxpl  9944  rankmapu  9947  rankxplim  9948  djuin  9987  infxpenlem  10082  ackbij1lem18  10305  cflm  10319  fin23lem29  10410  hsmexlem4  10498  hsmexlem5  10499  brdom3  10597  brdom5  10598  brdom4  10599  smobeth  10655  pwfseqlem3  10729  wundm  10797  wunrn  10798  wunex2  10807  ltsopi  10957  dmaddpi  10959  dmmulpi  10960  nqerf  10999  ltrelxr  11351  uzssre  12925  uzwo2  12977  infssuzle  12996  infssuzcl  12997  uzwo3  13008  nn0ssq  13022  nnssq  13023  qsscn  13025  rpnnen1lem3  13044  rpnnen1lem5  13046  dflt2  13210  ioosscn  13469  unitsscn  13560  fzval2  13570  fzossz  13736  fzossnn  13765  injresinj  13838  flval3  13866  uzsup  13914  uzrdgfni  14009  expcl2lem  14124  rpexpcl  14131  expge0  14149  expge1  14150  hashxrcl  14406  seqcoll  14513  xptrrel  15029  trclublem  15044  01sqrexlem3  15293  limsupval2  15526  limsupgre  15527  rlimpm  15546  rlimclim  15592  isercolllem1  15713  isercolllem2  15714  isercoll  15716  caurcvg  15725  caucvg  15727  summolem2a  15763  summolem2  15764  zsum  15766  fsumcvg3  15777  fsumrpcl  15785  fsumge0  15843  climfsum  15868  ackbijnn  15876  prodmolem2a  15982  prodmolem2  15983  zprod  15985  fprodrpcl  16004  fprodge0  16041  fprodge1  16043  rprisefaccl  16071  divalglem8  16448  sadaddlem  16512  lcmfval  16668  isprm3  16730  maxprmfct  16756  pclem  16885  prmreclem1  16963  prmreclem2  16964  prmreclem3  16965  1arith  16974  4sqlem11  17002  ramtlecl  17047  ramcl2lem  17056  ramxrcl  17064  prmgaplem3  17100  prmgaplem4  17101  cshwshashlem1  17143  structfn  17203  strleun  17204  ressbasss  17297  ressbasss2  17299  srngbase  17369  srngplusg  17370  srngmulr  17371  lmodbase  17385  lmodplusg  17386  lmodsca  17387  ipsbase  17396  ipsaddg  17397  ipsmulr  17398  ipssca  17399  ipsvsca  17400  ipsip  17401  phlbase  17406  phlplusg  17407  phlsca  17408  phlvsca  17409  phlip  17410  odrngbas  17463  odrngplusg  17464  odrngmulr  17465  odrngtset  17466  odrngle  17467  odrngds  17468  prdsvallem  17514  prdsval  17515  prdssca  17516  prdsbas  17517  prdsplusg  17518  prdsmulr  17519  prdsvsca  17520  prdsip  17521  prdsle  17522  prdsds  17524  prdstset  17526  prdshom  17527  prdsco  17528  imasbas  17572  imasds  17573  imasplusg  17577  imasmulr  17578  imassca  17579  imasvsca  17580  imasip  17581  imastset  17582  imasle  17583  wunfunc  17965  wunfuncOLD  17966  fullfunc  17973  fthfunc  17974  isfull  17977  isfth  17981  wunnat  18024  wunnatOLD  18025  dmcoass  18133  catcisolem  18177  catciso  18178  catcoppccl  18184  catcoppcclOLD  18185  catcfuccl  18186  catcfucclOLD  18187  catcxpccl  18276  catcxpcclOLD  18277  ipobas  18601  ipolerval  18602  ipotset  18603  psdmrn  18643  psss  18650  ledm  18660  lern  18661  dirdm  18670  dirge  18673  mulgfval  19109  mvdco  19487  f1omvdconj  19488  gexex  19895  gsumval3  19949  lssacs  20988  cnfldbas  21391  mpocnfldadd  21392  mpocnfldmul  21394  cnfldcj  21396  cnfldtset  21397  cnfldle  21398  cnfldds  21399  cnfldunif  21400  cnfldbasOLD  21406  cnfldaddOLD  21407  cnfldmulOLD  21408  cnfldcjOLD  21409  cnfldtsetOLD  21410  cnfldleOLD  21411  cnflddsOLD  21412  cnfldunifOLD  21413  rge0srg  21479  zntoslem  21598  asplss  21917  aspsubrg  21919  psrass1lem  21975  psrbas  21976  psrplusg  21979  psrmulr  21985  psrsca  21990  psrvscafval  21991  psrass1  22007  psrass23l  22010  psrcom  22011  psrass23  22012  psropprmul  22260  coe1mul2  22293  ofco2  22478  toponsspwpw  22949  dmtopon  22950  leordtval2  23241  lmbrf  23289  lmres  23329  fiuncmp  23433  comppfsc  23561  1stckgenlem  23582  kgencn3  23587  ptbasfi  23610  xkoopn  23618  txcnmpt  23653  txkgen  23681  opnfbas  23871  fmfnfmlem4  23986  tsmsxplem1  24182  trust  24259  restutop  24267  nmoffn  24753  nmofval  24756  nmogelb  24758  nmolb  24759  nmof  24761  qtopbas  24801  tgqioo  24841  re2ndc  24842  iitopon  24924  dfii3  24928  iimulcnOLD  24987  cnheiborlem  25005  bndth  25009  lebnumii  25017  reparphtiOLD  25049  pcoass  25076  cphsqrtcl  25237  lmmbrf  25315  iscauf  25333  caucfil  25336  lmclimf  25357  rrxmval  25458  rrxmet  25461  ovolfioo  25521  ovolficc  25522  ovolficcss  25523  ovolfsf  25525  ovollb  25533  ovolicc2lem3  25573  ovolicc2lem4  25574  ovolicc2  25576  volf  25583  volsup  25610  ovolfs2  25625  uniiccdif  25632  uniioovol  25633  uniiccvol  25634  uniioombllem2  25637  uniioombllem3a  25638  uniioombllem3  25639  uniioombllem4  25640  uniioombllem5  25641  uniioombl  25643  dyadmbllem  25653  dyadmbl  25654  opnmbllem  25655  opnmblALT  25657  volsup2  25659  vitalilem4  25665  vitalilem5  25666  vitali  25667  mbfimaopnlem  25709  mbflimsup  25720  i1f0  25741  i1f1  25744  itg11  25745  itg2mulc  25802  itg2gt0  25815  ellimc2  25932  limcresi  25940  dvreslem  25964  dvres2lem  25965  dvaddbr  25994  dvmulbr  25995  dvmulbrOLD  25996  dvlipcn  26053  c1liplem1  26055  lhop1lem  26072  lhop1  26073  lhop2  26074  lhop  26075  dvfsumrlim  26092  ftc1cn  26104  itgsubstlem  26109  itgsubst  26110  itgpowd  26111  mdegleb  26123  mdeglt  26124  mdegldg  26125  mdegxrcl  26126  mdegcl  26128  mdegaddle  26133  mdegmullem  26137  deg1mul3le  26176  ig1peu  26234  ig1pdvds  26239  aacjcl  26387  aannenlem2  26389  aannenlem3  26390  aalioulem2  26393  taylfval  26418  radcnvcl  26478  radcnvlt1  26479  radcnvle  26481  abelth  26503  abelth2  26504  pilem2  26514  pilem3  26515  pige3ALT  26580  recosf1o  26595  resinf1o  26596  tanord1  26597  logcn  26707  dvlog  26711  dvlog2lem  26712  efopn  26718  logtayl  26720  cxpcn3  26809  loglesqrt  26822  ssscongptld  26883  leibpi  27003  efrlim  27030  efrlimOLD  27031  jensenlem1  27048  jensenlem2  27049  jensen  27050  amgm  27052  lgamgulmlem2  27091  ftalem5  27138  efnnfsumcl  27164  efchtdvds  27220  mpodvdsmulf1o  27255  fsumdvdsmul  27256  dvdsmulf1o  27257  fsumdvdsmulOLD  27258  lgsfcl2  27365  2sqlem6  27485  2sqlem8  27488  2sqlem9  27489  rpvmasumlem  27549  rpvmasum2  27574  dchrisum0re  27575  dchrisum0lem3  27581  dchrisum0  27582  rplogsum  27589  dirith2  27590  noextendseq  27730  oldf  27914  leftssno  27937  rightssno  27938  addsbdaylem  28067  mulsproplem12  28171  mulsproplem13  28172  mulsproplem14  28173  mulsasslem3  28209  precsexlem11  28259  nnssno  28345  axtgcgrrflx  28488  axtgcgrid  28489  axtgsegcon  28490  axtg5seg  28491  axtgbtwnid  28492  axtgpasch  28493  axtgcont1  28494  tgcgr4  28557  motcgrg  28570  tglng  28572  upgrss  29123  pthdivtx  29765  disjxwwlkn  29946  ex-fpar  30494  nmlno0lem  30825  hlimcaui  31268  chsspwh  31279  shsss  31345  chintcli  31363  shsleji  31402  shub1i  31406  shsval2i  31419  lejdii  31570  spanuni  31576  sshhococi  31578  spansnpji  31610  osumcori  31675  5oai  31693  3oalem6  31699  3oai  31700  pjssmii  31713  mayete3i  31760  mayetes3i  31761  nmlnop0iALT  32027  imaelshi  32090  pjnmopi  32180  pjclem1  32227  pjci  32232  mdslmd1lem1  32357  shatomistici  32393  hatomistici  32394  chpssati  32395  xppreima  32664  iundisjfi  32801  iundisj2fi  32802  fprodex01  32829  xrsmulgzz  32992  fsumrp0cl  33007  gsummpt2co  33031  cycpmfv2  33107  cycpmrn  33136  rlocbas  33239  rlocaddval  33240  rlocmulval  33241  1fldgenq  33289  xrge0slmod  33341  lsmsnorb  33384  idlsrgbas  33497  idlsrgplusg  33498  idlsrgmulr  33500  idlsrgtset  33501  ordtconnlem1  33870  xrge0iifhom  33883  lmlimxrge0  33894  lmxrge0  33898  indsumin  33986  esumcst  34027  esumpfinvallem  34038  esumpfinval  34039  esumpfinvalf  34040  esumcvg  34050  imambfm  34227  elmbfmvol2  34232  sxbrsigalem3  34237  sxbrsigalem2  34251  sxbrsigalem4  34252  sitgclg  34307  eulerpartlem1  34332  eulerpartlemgvv  34341  eulerpartlemgh  34343  eulerpartlemgf  34344  ballotlemfc0  34457  ballotlemfcc  34458  ballotlemiex  34466  ballotlemsup  34469  ballotlemsima  34480  ballotlemrv2  34486  ballotth  34502  signsplypnf  34527  signsply0  34528  rpsqrtcn  34570  itgexpif  34583  fsum2dsub  34584  reprfi2  34600  chtvalz  34606  breprexplemc  34609  breprexpnat  34611  circlemeth  34617  circlemethnat  34618  circlevma  34619  circlemethhgt  34620  hgt750lemd  34625  hgt750lema  34634  tgoldbachgtde  34637  tgoldbachgtda  34638  tgoldbachgt  34640  bnj1145  34969  bnj1286  34995  subfacp1lem2a  35148  erdszelem4  35162  erdszelem5  35163  erdszelem7  35165  erdszelem8  35166  kur14lem7  35180  kur14lem9  35182  resconn  35214  iccllysconn  35218  txpss3v  35842  txprel  35843  limitssson  35875  finminlem  36284  tailf  36341  filnetlem3  36346  onint1  36415  bj-unrab  36892  bj-2upln1upl  36990  bj-imdirco  37156  bj-rvecssabl  37272  taupilem2  37288  taupi  37289  poimirlem3  37583  poimirlem30  37610  poimirlem31  37611  poimirlem32  37612  broucube  37614  opnmbllem0  37616  mblfinlem1  37617  mblfinlem2  37618  mblfinlem3  37619  mblfinlem4  37620  ismblfin  37621  mbfposadd  37627  cnambfre  37628  itg2addnc  37634  ftc1cnnclem  37651  ftc1cnnc  37652  ftc1anclem3  37655  ftc1anclem7  37659  ftc1anc  37661  ftc2nc  37662  dvreasin  37666  dvreacos  37667  areacirclem1  37668  areacirclem2  37669  areacirc  37673  caures  37720  reheibor  37799  xrnss3v  38328  xrnrel  38329  atlatmstc  39275  atlatle  39276  pmaple  39718  sspadd1  39772  sspadd2  39773  dvrelog2  42021  dvrelog3  42022  sumcubes  42301  diophin  42728  4rexfrabdioph  42754  6rexfrabdioph  42755  irrapxlem1  42778  irrapx1  42784  rmxyelqirr  42866  monotuz  42898  jm2.27dlem5  42970  hbtlem2  43081  algbase  43135  algaddg  43136  algmulr  43137  algsca  43138  algvsca  43139  arearect  43176  areaquad  43177  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  44266  lhe4.4ex1a  44298  uzmptshftfval  44315  binomcxplemdvbinom  44322  binomcxplemcvg  44323  binomcxplemnotnn0  44325  relopabVD  44872  dmwf  44913  rnwf  44914  fzisoeu  45215  fzsscn  45226  fzssre  45229  fzossuz  45296  zssxr  45312  uzssre2  45322  supminfxr  45379  uzsscn  45391  rpssxr  45396  uzinico  45478  limcresiooub  45563  limcresioolb  45564  limcleqr  45565  limclner  45572  limclr  45576  limsupequzmpt2  45639  liminfval2  45689  liminfequzmpt2  45712  icccncfext  45808  cncficcgt0  45809  ioodvbdlimc1lem2  45853  ioodvbdlimc2lem  45855  dvnprodlem1  45867  dvnprodlem2  45868  itgsin0pilem1  45871  itgsinexplem1  45875  itgsinexp  45876  dirkercncflem2  46025  fourierdlem16  46044  fourierdlem18  46046  fourierdlem20  46048  fourierdlem21  46049  fourierdlem22  46050  fourierdlem25  46053  fourierdlem37  46065  fourierdlem42  46070  fourierdlem50  46077  fourierdlem52  46079  fourierdlem62  46089  fourierdlem64  46091  fourierdlem66  46093  fourierdlem68  46095  fourierdlem74  46101  fourierdlem75  46102  fourierdlem76  46103  fourierdlem79  46106  fourierdlem83  46110  fourierdlem95  46122  fourierdlem101  46128  fourierdlem102  46129  fourierdlem103  46130  fourierdlem104  46131  fourierdlem112  46139  fourierdlem114  46141  sqwvfoura  46149  sqwvfourb  46150  fouriersw  46152  etransclem24  46179  etransclem48  46203  sge0sn  46300  sge0tsms  46301  sge0f1o  46303  sge0pr  46315  sge0resplit  46327  sge0split  46330  sge0iunmptlemre  46336  sge0isummpt2  46353  carageniuncllem1  46442  hoicvr  46469  hoicvrrex  46477  hoidmvlelem2  46517  hspmbl  46550  smfmullem4  46715  prmdvdsfmtnof1lem1  47458  prmdvdsfmtnof  47460  oddibas  47896  2zrngbas  47965  2zrng0  47967  sepfsepc  48607  aacllem  48895  amgmlemALT  48897