Theorem sstri 3956

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

Syntax hints:   ⊆ wss 3914

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 3931

This theorem is referenced by:  snsstp1  4780  snsstp2  4781  uniintsn  4949  elopabran  5522  ssrnres  6151  cossxp  6245  foimacnv  6817  ssimaex  6946  riotassuni  7384  oprabss  7497  dmexg  7877  rnexg  7878  fabexgOLD  7915  mptmpoopabbrd  8059  fparlem3  8093  fparlem4  8094  snopsuppss  8158  tposssxp  8209  naddunif  8657  naddasslem1  8658  naddasslem2  8659  mapsspw  8851  sbthlem5  9055  sbthlem7  9057  cnvimamptfin  9304  marypha1lem  9384  ordtypelem4  9474  hartogslem1  9495  ttrclco  9671  cottrcl  9672  tc2  9695  frmin  9702  frrlem16  9711  tz9.12lem1  9740  rankval4  9820  rankxpl  9828  rankmapu  9831  rankxplim  9832  djuin  9871  infxpenlem  9966  ackbij1lem18  10189  cflm  10203  fin23lem29  10294  hsmexlem4  10382  hsmexlem5  10383  brdom3  10481  brdom5  10482  brdom4  10483  smobeth  10539  pwfseqlem3  10613  wundm  10681  wunrn  10682  wunex2  10691  ltsopi  10841  dmaddpi  10843  dmmulpi  10844  nqerf  10883  ltrelxr  11235  uzssre  12815  uzwo2  12871  infssuzle  12890  infssuzcl  12891  uzwo3  12902  nn0ssq  12916  nnssq  12917  qsscn  12919  rpnnen1lem3  12938  rpnnen1lem5  12940  dflt2  13108  ioosscn  13369  unitsscn  13461  fzval2  13471  fzossz  13640  fzossnn  13672  injresinj  13749  flval3  13777  uzsup  13825  uzrdgfni  13923  expcl2lem  14038  rpexpcl  14045  expge0  14063  expge1  14064  hashxrcl  14322  seqcoll  14429  xptrrel  14946  trclublem  14961  01sqrexlem3  15210  limsupval2  15446  limsupgre  15447  rlimpm  15466  rlimclim  15512  isercolllem1  15631  isercolllem2  15632  isercoll  15634  caurcvg  15643  caucvg  15645  summolem2a  15681  summolem2  15682  zsum  15684  fsumcvg3  15695  fsumrpcl  15703  fsumge0  15761  climfsum  15786  ackbijnn  15794  prodmolem2a  15900  prodmolem2  15901  zprod  15903  fprodrpcl  15922  fprodge0  15959  fprodge1  15961  rprisefaccl  15989  divalglem8  16370  sadaddlem  16436  lcmfval  16591  isprm3  16653  maxprmfct  16679  pclem  16809  prmreclem1  16887  prmreclem2  16888  prmreclem3  16889  1arith  16898  4sqlem11  16926  ramtlecl  16971  ramcl2lem  16980  ramxrcl  16988  prmgaplem3  17024  prmgaplem4  17025  cshwshashlem1  17066  structfn  17126  strleun  17127  ressbasss  17209  ressbasss2  17211  srngbase  17273  srngplusg  17274  srngmulr  17275  lmodbase  17289  lmodplusg  17290  lmodsca  17291  ipsbase  17300  ipsaddg  17301  ipsmulr  17302  ipssca  17303  ipsvsca  17304  ipsip  17305  phlbase  17310  phlplusg  17311  phlsca  17312  phlvsca  17313  phlip  17314  odrngbas  17367  odrngplusg  17368  odrngmulr  17369  odrngtset  17370  odrngle  17371  odrngds  17372  prdsvallem  17417  prdsval  17418  prdssca  17419  prdsbas  17420  prdsplusg  17421  prdsmulr  17422  prdsvsca  17423  prdsip  17424  prdsle  17425  prdsds  17427  prdstset  17429  prdshom  17430  prdsco  17431  imasbas  17475  imasds  17476  imasplusg  17480  imasmulr  17481  imassca  17482  imasvsca  17483  imasip  17484  imastset  17485  imasle  17486  wunfunc  17863  fullfunc  17870  fthfunc  17871  isfull  17874  isfth  17878  wunnat  17921  dmcoass  18028  catcisolem  18072  catciso  18073  catcoppccl  18079  catcfuccl  18080  catcxpccl  18168  ipobas  18490  ipolerval  18491  ipotset  18492  psdmrn  18532  psss  18539  ledm  18549  lern  18550  dirdm  18559  dirge  18562  mulgfval  19001  mvdco  19375  f1omvdconj  19376  gexex  19783  gsumval3  19837  lssacs  20873  cnfldbas  21268  mpocnfldadd  21269  mpocnfldmul  21271  cnfldcj  21273  cnfldtset  21274  cnfldle  21275  cnfldds  21276  cnfldunif  21277  cnfldbasOLD  21283  cnfldaddOLD  21284  cnfldmulOLD  21285  cnfldcjOLD  21286  cnfldtsetOLD  21287  cnfldleOLD  21288  cnflddsOLD  21289  cnfldunifOLD  21290  rge0srg  21355  zntoslem  21466  asplss  21783  aspsubrg  21785  psrass1lem  21841  psrbas  21842  psrplusg  21845  psrmulr  21851  psrsca  21856  psrvscafval  21857  psrass1  21873  psrass23l  21876  psrcom  21877  psrass23  21878  psropprmul  22122  coe1mul2  22155  ofco2  22338  toponsspwpw  22809  dmtopon  22810  leordtval2  23099  lmbrf  23147  lmres  23187  fiuncmp  23291  comppfsc  23419  1stckgenlem  23440  kgencn3  23445  ptbasfi  23468  xkoopn  23476  txcnmpt  23511  txkgen  23539  opnfbas  23729  fmfnfmlem4  23844  tsmsxplem1  24040  trust  24117  restutop  24125  nmoffn  24599  nmofval  24602  nmogelb  24604  nmolb  24605  nmof  24607  qtopbas  24647  tgqioo  24688  re2ndc  24689  iitopon  24772  dfii3  24776  iimulcnOLD  24835  cnheiborlem  24853  bndth  24857  lebnumii  24865  reparphtiOLD  24897  pcoass  24924  cphsqrtcl  25084  lmmbrf  25162  iscauf  25180  caucfil  25183  lmclimf  25204  rrxmval  25305  rrxmet  25308  ovolfioo  25368  ovolficc  25369  ovolficcss  25370  ovolfsf  25372  ovollb  25380  ovolicc2lem3  25420  ovolicc2lem4  25421  ovolicc2  25423  volf  25430  volsup  25457  ovolfs2  25472  uniiccdif  25479  uniioovol  25480  uniiccvol  25481  uniioombllem2  25484  uniioombllem3a  25485  uniioombllem3  25486  uniioombllem4  25487  uniioombllem5  25488  uniioombl  25490  dyadmbllem  25500  dyadmbl  25501  opnmbllem  25502  opnmblALT  25504  volsup2  25506  vitalilem4  25512  vitalilem5  25513  vitali  25514  mbfimaopnlem  25556  mbflimsup  25567  i1f0  25588  i1f1  25591  itg11  25592  itg2mulc  25648  itg2gt0  25661  ellimc2  25778  limcresi  25786  dvreslem  25810  dvres2lem  25811  dvaddbr  25840  dvmulbr  25841  dvmulbrOLD  25842  dvlipcn  25899  c1liplem1  25901  lhop1lem  25918  lhop1  25919  lhop2  25920  lhop  25921  dvfsumrlim  25938  ftc1cn  25950  itgsubstlem  25955  itgsubst  25956  itgpowd  25957  mdegleb  25969  mdeglt  25970  mdegldg  25971  mdegxrcl  25972  mdegcl  25974  mdegaddle  25979  mdegmullem  25983  deg1mul3le  26022  ig1peu  26080  ig1pdvds  26085  aacjcl  26235  aannenlem2  26237  aannenlem3  26238  aalioulem2  26241  taylfval  26266  radcnvcl  26326  radcnvlt1  26327  radcnvle  26329  abelth  26351  abelth2  26352  pilem2  26362  pilem3  26363  pige3ALT  26429  recosf1o  26444  resinf1o  26445  tanord1  26446  logcn  26556  dvlog  26560  dvlog2lem  26561  efopn  26567  logtayl  26569  cxpcn3  26658  loglesqrt  26671  ssscongptld  26732  leibpi  26852  efrlim  26879  efrlimOLD  26880  jensenlem1  26897  jensenlem2  26898  jensen  26899  amgm  26901  lgamgulmlem2  26940  ftalem5  26987  efnnfsumcl  27013  efchtdvds  27069  mpodvdsmulf1o  27104  fsumdvdsmul  27105  dvdsmulf1o  27106  fsumdvdsmulOLD  27107  lgsfcl2  27214  2sqlem6  27334  2sqlem8  27337  2sqlem9  27338  rpvmasumlem  27398  rpvmasum2  27423  dchrisum0re  27424  dchrisum0lem3  27430  dchrisum0  27431  rplogsum  27438  dirith2  27439  noextendseq  27579  oldf  27765  leftssno  27792  rightssno  27793  addsbdaylem  27923  mulsproplem12  28030  mulsproplem13  28031  mulsproplem14  28032  mulsasslem3  28068  precsexlem11  28119  onscutlt  28165  bdayon  28173  nnssno  28215  axtgcgrrflx  28389  axtgcgrid  28390  axtgsegcon  28391  axtg5seg  28392  axtgbtwnid  28393  axtgpasch  28394  axtgcont1  28395  tgcgr4  28458  motcgrg  28471  tglng  28473  upgrss  29015  pthdivtx  29657  disjxwwlkn  29843  ex-fpar  30391  nmlno0lem  30722  hlimcaui  31165  chsspwh  31176  shsss  31242  chintcli  31260  shsleji  31299  shub1i  31303  shsval2i  31316  lejdii  31467  spanuni  31473  sshhococi  31475  spansnpji  31507  osumcori  31572  5oai  31590  3oalem6  31596  3oai  31597  pjssmii  31610  mayete3i  31657  mayetes3i  31658  nmlnop0iALT  31924  imaelshi  31987  pjnmopi  32077  pjclem1  32124  pjci  32129  mdslmd1lem1  32254  shatomistici  32290  hatomistici  32291  chpssati  32292  xppreima  32569  iundisjfi  32719  iundisj2fi  32720  fprodex01  32750  indsumin  32785  xrsmulgzz  32947  fsumrp0cl  32962  gsummpt2co  32988  cycpmfv2  33071  cycpmrn  33100  rlocbas  33218  rlocaddval  33219  rlocmulval  33220  1fldgenq  33272  xrge0slmod  33319  lsmsnorb  33362  idlsrgbas  33475  idlsrgplusg  33476  idlsrgmulr  33478  idlsrgtset  33479  constrextdg2  33739  ordtconnlem1  33914  xrge0iifhom  33927  lmlimxrge0  33938  lmxrge0  33942  esumcst  34053  esumpfinvallem  34064  esumpfinval  34065  esumpfinvalf  34066  esumcvg  34076  imambfm  34253  elmbfmvol2  34258  sxbrsigalem3  34263  sxbrsigalem2  34277  sxbrsigalem4  34278  sitgclg  34333  eulerpartlem1  34358  eulerpartlemgvv  34367  eulerpartlemgh  34369  eulerpartlemgf  34370  ballotlemfc0  34484  ballotlemfcc  34485  ballotlemiex  34493  ballotlemsup  34496  ballotlemsima  34507  ballotlemrv2  34513  ballotth  34529  signsplypnf  34541  signsply0  34542  rpsqrtcn  34584  itgexpif  34597  fsum2dsub  34598  reprfi2  34614  chtvalz  34620  breprexplemc  34623  breprexpnat  34625  circlemeth  34631  circlemethnat  34632  circlevma  34633  circlemethhgt  34634  hgt750lemd  34639  hgt750lema  34648  tgoldbachgtde  34651  tgoldbachgtda  34652  tgoldbachgt  34654  bnj1145  34983  bnj1286  35009  subfacp1lem2a  35167  erdszelem4  35181  erdszelem5  35182  erdszelem7  35184  erdszelem8  35185  kur14lem7  35199  kur14lem9  35201  resconn  35233  iccllysconn  35237  txpss3v  35866  txprel  35867  limitssson  35899  finminlem  36306  tailf  36363  filnetlem3  36368  onint1  36437  bj-unrab  36914  bj-2upln1upl  37012  bj-imdirco  37178  bj-rvecssabl  37294  taupilem2  37310  taupi  37311  poimirlem3  37617  poimirlem30  37644  poimirlem31  37645  poimirlem32  37646  broucube  37648  opnmbllem0  37650  mblfinlem1  37651  mblfinlem2  37652  mblfinlem3  37653  mblfinlem4  37654  ismblfin  37655  mbfposadd  37661  cnambfre  37662  itg2addnc  37668  ftc1cnnclem  37685  ftc1cnnc  37686  ftc1anclem3  37689  ftc1anclem7  37693  ftc1anc  37695  ftc2nc  37696  dvreasin  37700  dvreacos  37701  areacirclem1  37702  areacirclem2  37703  areacirc  37707  caures  37754  reheibor  37833  xrnss3v  38354  xrnrel  38355  atlatmstc  39312  atlatle  39313  pmaple  39755  sspadd1  39809  sspadd2  39810  dvrelog2  42052  dvrelog3  42053  rpsscn  42287  sumcubes  42301  redvmptabs  42348  diophin  42760  4rexfrabdioph  42786  6rexfrabdioph  42787  irrapxlem1  42810  irrapx1  42816  rmxyelqirr  42898  monotuz  42930  jm2.27dlem5  43002  hbtlem2  43113  algbase  43163  algaddg  43164  algmulr  43165  algsca  43166  algvsca  43167  arearect  43204  areaquad  43205  rtrclex  43606  trclubgNEW  43607  trclexi  43609  rtrclexi  43610  cnvtrcl0  43615  dfrtrcl5  43618  trrelsuperrel2dg  43660  relexpaddss  43707  brtrclfv2  43716  frege131d  43753  xphe  43770  clsk3nimkb  44029  gneispace  44123  k0004val0  44143  inaex  44286  lhe4.4ex1a  44318  uzmptshftfval  44335  binomcxplemdvbinom  44342  binomcxplemcvg  44343  binomcxplemnotnn0  44345  relopabVD  44890  dmwf  44955  rnwf  44956  fzisoeu  45298  fzsscn  45309  fzssre  45312  fzossuz  45377  zssxr  45393  uzssre2  45403  supminfxr  45460  uzsscn  45471  rpssxr  45476  uzinico  45557  limcresiooub  45640  limcresioolb  45641  limcleqr  45642  limclner  45649  limclr  45653  limsupequzmpt2  45716  liminfval2  45766  liminfequzmpt2  45789  icccncfext  45885  cncficcgt0  45886  ioodvbdlimc1lem2  45930  ioodvbdlimc2lem  45932  dvnprodlem2  45945  itgsin0pilem1  45948  itgsinexplem1  45952  itgsinexp  45953  dirkercncflem2  46102  fourierdlem16  46121  fourierdlem18  46123  fourierdlem20  46125  fourierdlem21  46126  fourierdlem22  46127  fourierdlem25  46130  fourierdlem37  46142  fourierdlem42  46147  fourierdlem50  46154  fourierdlem52  46156  fourierdlem62  46166  fourierdlem64  46168  fourierdlem66  46170  fourierdlem68  46172  fourierdlem74  46178  fourierdlem75  46179  fourierdlem76  46180  fourierdlem79  46183  fourierdlem83  46187  fourierdlem95  46199  fourierdlem101  46205  fourierdlem102  46206  fourierdlem103  46207  fourierdlem104  46208  fourierdlem112  46216  fourierdlem114  46218  sqwvfoura  46226  sqwvfourb  46227  fouriersw  46229  etransclem24  46256  etransclem48  46280  sge0sn  46377  sge0tsms  46378  sge0f1o  46380  sge0pr  46392  sge0resplit  46404  sge0split  46407  sge0iunmptlemre  46413  sge0isummpt2  46430  carageniuncllem1  46519  hoicvr  46546  hoicvrrex  46554  hoidmvlelem2  46594  hspmbl  46627  smfmullem4  46792  lamberte  46889  rehalfge1  47336  prmdvdsfmtnof1lem1  47585  prmdvdsfmtnof  47587  upgrimpthslem2  47908  upgrimpths  47909  oddibas  48161  2zrngbas  48230  2zrng0  48232  dmtposss  48864  tposres3  48869  sepfsepc  48916  uptrlem1  49199  uptrlem2  49200  uptrlem3  49201  uptra  49204  uptrar  49205  uobeqw  49208  uptr2  49210  uptr2a  49211  fucoppcfunc  49401  aacllem  49790  amgmlemALT  49792