Theorem sstri 3931

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 1802  ax-4 1816

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

This theorem is referenced by:  snsstp1  4754  snsstp2  4755  uniintsn  4922  elopabran  5510  ssrnres  6136  cossxp  6230  foimacnv  6791  ssimaex  6919  riotassuni  7360  oprabss  7471  dmexg  7848  rnexg  7849  fabexgOLD  7886  mptmpoopabbrd  8029  fparlem3  8060  fparlem4  8061  snopsuppss  8126  tposssxp  8177  naddunif  8626  naddasslem1  8627  naddasslem2  8628  mapsspw  8823  sbthlem5  9026  sbthlem7  9028  cnvimamptfin  9260  marypha1lem  9343  ordtypelem4  9433  hartogslem1  9454  ttrclco  9637  cottrcl  9638  tc2  9659  frmin  9671  frrlem16  9680  tz9.12lem1  9709  rankval4  9789  rankxpl  9797  rankmapu  9800  rankxplim  9801  djuin  9840  infxpenlem  9933  ackbij1lem18  10156  cflm  10170  fin23lem29  10261  hsmexlem4  10349  hsmexlem5  10350  brdom3  10448  brdom5  10449  brdom4  10450  smobeth  10507  pwfseqlem3  10581  wundm  10649  wunrn  10650  wunex2  10659  ltsopi  10809  dmaddpi  10811  dmmulpi  10812  nqerf  10851  ltrelxr  11204  uzssre  12808  uzwo2  12860  infssuzle  12879  infssuzcl  12880  uzwo3  12891  nn0ssq  12905  nnssq  12906  qsscn  12908  rpnnen1lem3  12927  rpnnen1lem5  12929  dflt2  13097  ioosscn  13359  unitsscn  13451  fzval2  13462  fzossz  13632  fzossnn  13664  injresinj  13744  flval3  13772  uzsup  13820  uzrdgfni  13918  expcl2lem  14033  rpexpcl  14040  expge0  14058  expge1  14059  hashxrcl  14317  seqcoll  14424  xptrrel  14940  trclublem  14955  01sqrexlem3  15204  limsupval2  15440  limsupgre  15441  rlimpm  15460  rlimclim  15506  isercolllem1  15625  isercolllem2  15626  isercoll  15628  caurcvg  15637  caucvg  15639  summolem2a  15675  summolem2  15676  zsum  15678  fsumcvg3  15689  fsumrpcl  15697  fsumge0  15756  climfsum  15781  ackbijnn  15791  prodmolem2a  15897  prodmolem2  15898  zprod  15900  fprodrpcl  15919  fprodge0  15956  fprodge1  15958  rprisefaccl  15986  divalglem8  16367  sadaddlem  16433  lcmfval  16588  isprm3  16650  maxprmfct  16677  pclem  16807  prmreclem1  16885  prmreclem2  16886  prmreclem3  16887  1arith  16896  4sqlem11  16924  ramtlecl  16969  ramcl2lem  16978  ramxrcl  16986  prmgaplem3  17022  prmgaplem4  17023  cshwshashlem1  17064  structfn  17124  strleun  17125  ressbasss  17207  ressbasss2  17209  srngbase  17271  srngplusg  17272  srngmulr  17273  lmodbase  17287  lmodplusg  17288  lmodsca  17289  ipsbase  17298  ipsaddg  17299  ipsmulr  17300  ipssca  17301  ipsvsca  17302  ipsip  17303  phlbase  17308  phlplusg  17309  phlsca  17310  phlvsca  17311  phlip  17312  odrngbas  17365  odrngplusg  17366  odrngmulr  17367  odrngtset  17368  odrngle  17369  odrngds  17370  prdsvallem  17415  prdsval  17416  prdssca  17417  prdsbas  17418  prdsplusg  17419  prdsmulr  17420  prdsvsca  17421  prdsip  17422  prdsle  17423  prdsds  17425  prdstset  17427  prdshom  17428  prdsco  17429  imasbas  17474  imasds  17475  imasplusg  17479  imasmulr  17480  imassca  17481  imasvsca  17482  imasip  17483  imastset  17484  imasle  17485  wunfunc  17866  fullfunc  17873  fthfunc  17874  isfull  17877  isfth  17881  wunnat  17924  dmcoass  18031  catcisolem  18075  catciso  18076  catcoppccl  18082  catcfuccl  18083  catcxpccl  18171  ipobas  18495  ipolerval  18496  ipotset  18497  psdmrn  18537  psss  18544  ledm  18554  lern  18555  dirdm  18564  dirge  18567  mulgfval  19043  mvdco  19418  f1omvdconj  19419  gexex  19826  gsumval3  19880  lssacs  20964  cnfldbas  21358  mpocnfldadd  21359  mpocnfldmul  21361  cnfldcj  21363  cnfldtset  21364  cnfldle  21365  cnfldds  21366  cnfldunif  21367  rge0srg  21420  zntoslem  21538  asplss  21855  aspsubrg  21857  psrass1lem  21915  psrbas  21916  psrplusg  21919  psrmulr  21924  psrsca  21929  psrvscafval  21930  psrass1  21945  psrass23l  21948  psrcom  21949  psrass23  21950  psropprmul  22229  coe1mul2  22262  ofco2  22441  toponsspwpw  22912  dmtopon  22913  leordtval2  23202  lmbrf  23250  lmres  23290  fiuncmp  23394  comppfsc  23522  1stckgenlem  23543  kgencn3  23548  ptbasfi  23571  xkoopn  23579  txcnmpt  23614  txkgen  23642  opnfbas  23832  fmfnfmlem4  23947  tsmsxplem1  24143  trust  24219  restutop  24227  nmoffn  24701  nmofval  24704  nmogelb  24706  nmolb  24707  nmof  24709  qtopbas  24749  tgqioo  24790  re2ndc  24791  iitopon  24871  dfii3  24875  cnheiborlem  24946  bndth  24950  lebnumii  24958  pcoass  25016  cphsqrtcl  25176  lmmbrf  25254  iscauf  25272  caucfil  25275  lmclimf  25296  rrxmval  25397  rrxmet  25400  ovolfioo  25459  ovolficc  25460  ovolficcss  25461  ovolfsf  25463  ovollb  25471  ovolicc2lem3  25511  ovolicc2lem4  25512  ovolicc2  25514  volf  25521  volsup  25548  ovolfs2  25563  uniiccdif  25570  uniioovol  25571  uniiccvol  25572  uniioombllem2  25575  uniioombllem3a  25576  uniioombllem3  25577  uniioombllem4  25578  uniioombllem5  25579  uniioombl  25581  dyadmbllem  25591  dyadmbl  25592  opnmbllem  25593  opnmblALT  25595  volsup2  25597  vitalilem4  25603  vitalilem5  25604  vitali  25605  mbfimaopnlem  25647  mbflimsup  25658  i1f0  25679  i1f1  25682  itg11  25683  itg2mulc  25739  itg2gt0  25752  ellimc2  25869  limcresi  25877  dvreslem  25901  dvres2lem  25902  dvaddbr  25930  dvmulbr  25931  dvlipcn  25986  c1liplem1  25988  lhop1lem  26005  lhop1  26006  lhop2  26007  lhop  26008  dvfsumrlim  26023  ftc1cn  26035  itgsubstlem  26040  itgsubst  26041  itgpowd  26042  mdegleb  26054  mdeglt  26055  mdegldg  26056  mdegxrcl  26057  mdegcl  26059  mdegaddle  26064  mdegmullem  26068  deg1mul3le  26107  ig1peu  26165  ig1pdvds  26170  aacjcl  26318  aannenlem2  26320  aannenlem3  26321  aalioulem2  26324  taylfval  26349  radcnvcl  26407  radcnvlt1  26408  radcnvle  26410  abelth  26431  abelth2  26432  pilem2  26442  pilem3  26443  pige3ALT  26509  recosf1o  26524  resinf1o  26525  tanord1  26526  logcn  26636  dvlog  26640  dvlog2lem  26641  efopn  26647  logtayl  26649  cxpcn3  26737  loglesqrt  26750  ssscongptld  26811  leibpi  26931  efrlim  26958  jensenlem1  26975  jensenlem2  26976  jensen  26977  amgm  26979  lgamgulmlem2  27018  ftalem5  27065  efnnfsumcl  27091  efchtdvds  27147  mpodvdsmulf1o  27182  fsumdvdsmul  27183  dvdsmulf1o  27184  lgsfcl2  27291  2sqlem6  27411  2sqlem8  27414  2sqlem9  27415  rpvmasumlem  27475  rpvmasum2  27500  dchrisum0re  27501  dchrisum0lem3  27507  dchrisum0  27508  rplogsum  27515  dirith2  27516  noextendseq  27656  oldf  27854  leftssno  27890  rightssno  27891  addbdaylem  28034  mulsproplem12  28144  mulsproplem13  28145  mulsproplem14  28146  mulsasslem3  28182  precsexlem11  28234  oncutlt  28281  bdayons  28293  nnssno  28339  axtgcgrrflx  28555  axtgcgrid  28556  axtgsegcon  28557  axtg5seg  28558  axtgbtwnid  28559  axtgpasch  28560  axtgcont1  28561  tgcgr4  28624  motcgrg  28637  tglng  28639  upgrss  29182  pthdivtx  29820  disjxwwlkn  30006  ex-fpar  30557  nmlno0lem  30889  hlimcaui  31332  chsspwh  31343  shsss  31409  chintcli  31427  shsleji  31466  shub1i  31470  shsval2i  31483  lejdii  31634  spanuni  31640  sshhococi  31642  spansnpji  31674  osumcori  31739  5oai  31757  3oalem6  31763  3oai  31764  pjssmii  31777  mayete3i  31824  mayetes3i  31825  nmlnop0iALT  32091  imaelshi  32154  pjnmopi  32244  pjclem1  32291  pjci  32296  mdslmd1lem1  32421  shatomistici  32457  hatomistici  32458  chpssati  32459  xppreima  32744  iundisjfi  32895  iundisj2fi  32896  fprodex01  32924  indsumin  32947  xrsmulgzz  33095  fsumrp0cl  33107  gsummpt2co  33136  cycpmfv2  33202  cycpmrn  33231  rlocbas  33355  rlocaddval  33356  rlocmulval  33357  1fldgenq  33413  xrge0slmod  33438  lsmsnorb  33481  idlsrgbas  33594  idlsrgplusg  33595  idlsrgmulr  33597  idlsrgtset  33598  selvply1rhmlemb  33710  esplyind  33766  vietalem  33770  constrextdg2  33940  ordtconnlem1  34115  xrge0iifhom  34128  lmlimxrge0  34139  lmxrge0  34143  esumcst  34254  esumpfinvallem  34265  esumpfinval  34266  esumpfinvalf  34267  esumcvg  34277  imambfm  34453  elmbfmvol2  34458  sxbrsigalem3  34463  sxbrsigalem2  34477  sxbrsigalem4  34478  sitgclg  34533  eulerpartlem1  34558  eulerpartlemgvv  34567  eulerpartlemgh  34569  eulerpartlemgf  34570  ballotlemfc0  34684  ballotlemfcc  34685  ballotlemiex  34693  ballotlemsup  34696  ballotlemsima  34707  ballotlemrv2  34713  ballotth  34729  signsplypnf  34741  signsply0  34742  rpsqrtcn  34784  itgexpif  34797  fsum2dsub  34798  reprfi2  34814  chtvalz  34820  breprexplemc  34823  breprexpnat  34825  circlemeth  34831  circlemethnat  34832  circlevma  34833  circlemethhgt  34834  hgt750lemd  34839  hgt750lema  34848  tgoldbachgtde  34851  tgoldbachgtda  34852  tgoldbachgt  34854  bnj1145  35182  bnj1286  35208  subfacp1lem2a  35415  erdszelem4  35429  erdszelem5  35430  erdszelem7  35432  erdszelem8  35433  kur14lem7  35447  kur14lem9  35449  resconn  35481  iccllysconn  35485  txpss3v  36111  txprel  36112  limitssson  36144  finminlem  36553  tailf  36610  filnetlem3  36615  onint1  36684  ttcuniun  36745  bj-unrab  37286  bj-2upln1upl  37384  bj-imdirco  37557  bj-rvecssabl  37673  taupilem2  37689  taupi  37690  poimirlem3  37997  poimirlem30  38024  poimirlem31  38025  poimirlem32  38026  broucube  38028  opnmbllem0  38030  mblfinlem1  38031  mblfinlem2  38032  mblfinlem3  38033  mblfinlem4  38034  ismblfin  38035  mbfposadd  38041  cnambfre  38042  itg2addnc  38048  ftc1cnnclem  38065  ftc1cnnc  38066  ftc1anclem3  38069  ftc1anclem7  38073  ftc1anc  38075  ftc2nc  38076  dvreasin  38080  dvreacos  38081  areacirclem1  38082  areacirclem2  38083  areacirc  38087  caures  38134  reheibor  38213  xrnss3v  38755  xrnrel  38756  atlatmstc  39818  atlatle  39819  pmaple  40260  sspadd1  40314  sspadd2  40315  dvrelog2  42556  dvrelog3  42557  rpsscn  42783  sumcubes  42797  redvmptabs  42844  diophin  43228  4rexfrabdioph  43250  6rexfrabdioph  43251  irrapxlem1  43274  irrapx1  43280  rmxyelqirr  43362  monotuz  43393  jm2.27dlem5  43465  hbtlem2  43576  algbase  43626  algaddg  43627  algmulr  43628  algsca  43629  algvsca  43630  arearect  43667  areaquad  43668  rtrclex  44068  trclubgNEW  44069  trclexi  44071  rtrclexi  44072  cnvtrcl0  44077  dfrtrcl5  44080  trrelsuperrel2dg  44122  relexpaddss  44169  brtrclfv2  44178  frege131d  44215  xphe  44232  clsk3nimkb  44491  gneispace  44585  k0004val0  44605  inaex  44748  lhe4.4ex1a  44780  uzmptshftfval  44797  binomcxplemdvbinom  44804  binomcxplemcvg  44805  binomcxplemnotnn0  44807  relopabVD  45351  dmwf  45416  rnwf  45417  fzisoeu  45755  fzsscn  45766  fzssre  45769  fzossuz  45832  zssxr  45848  uzssre2  45857  supminfxr  45914  uzsscn  45925  rpssxr  45930  uzinico  46011  limcresiooub  46092  limcresioolb  46093  limcleqr  46094  limclner  46101  limclr  46105  limsupequzmpt2  46168  liminfval2  46218  liminfequzmpt2  46241  icccncfext  46337  cncficcgt0  46338  ioodvbdlimc1lem2  46382  ioodvbdlimc2lem  46384  dvnprodlem2  46397  itgsin0pilem1  46400  itgsinexplem1  46404  itgsinexp  46405  dirkercncflem2  46554  fourierdlem16  46573  fourierdlem18  46575  fourierdlem20  46577  fourierdlem21  46578  fourierdlem22  46579  fourierdlem25  46582  fourierdlem37  46594  fourierdlem42  46599  fourierdlem50  46606  fourierdlem52  46608  fourierdlem62  46618  fourierdlem64  46620  fourierdlem66  46622  fourierdlem68  46624  fourierdlem74  46630  fourierdlem75  46631  fourierdlem76  46632  fourierdlem79  46635  fourierdlem83  46639  fourierdlem95  46651  fourierdlem101  46657  fourierdlem102  46658  fourierdlem103  46659  fourierdlem104  46660  fourierdlem112  46668  fourierdlem114  46670  sqwvfoura  46678  sqwvfourb  46679  fouriersw  46681  etransclem24  46708  etransclem48  46732  sge0sn  46829  sge0tsms  46830  sge0f1o  46832  sge0pr  46844  sge0resplit  46856  sge0split  46859  sge0iunmptlemre  46865  sge0isummpt2  46882  carageniuncllem1  46971  hoicvr  46998  hoicvrrex  47006  hoidmvlelem2  47046  hspmbl  47079  smfmullem4  47244  chnsuslle  47333  lamberte  47358  rehalfge1  47809  prmdvdsfmtnof1lem1  48069  prmdvdsfmtnof  48071  upgrimpthslem2  48406  upgrimpths  48407  oddibas  48671  2zrngbas  48740  2zrng0  48742  dmtposss  49373  tposres3  49378  sepfsepc  49425  uptrlem1  49707  uptrlem2  49708  uptrlem3  49709  uptra  49712  uptrar  49713  uobeqw  49716  uptr2  49718  uptr2a  49719  fucoppcfunc  49909  aacllem  50298  amgmlemALT  50300