Theorem sstri 3947

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

Syntax hints:   ⊆ wss 3906

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

This theorem depends on definitions:  df-bi 210  df-ss 3923

This theorem is referenced by:  snsstp1  4783  snsstp2  4784  uniintsn  4951  elopabran  5548  ssrnres  6178  cossxp  6275  foimacnv  6840  ssimaex  6968  riotassuni  7409  oprabss  7520  dmexg  7899  rnexg  7900  mptmpoopabbrd  8079  fparlem3  8110  fparlem4  8111  snopsuppss  8176  tposssxp  8227  naddunif  8681  naddasslem1  8682  naddasslem2  8683  mapsspw  8877  sbthlem5  9080  sbthlem7  9082  cnvimamptfin  9311  marypha1lem  9394  ordtypelem4  9484  hartogslem1  9505  ttrclco  9688  cottrcl  9689  tc2  9710  frmin  9722  frrlem16  9731  tz9.12lem1  9760  rankval4  9840  rankxpl  9848  rankmapu  9851  rankxplim  9852  djuin  9905  infxpenlem  9998  ackbij1lem18  10220  cflm  10234  fin23lem29  10326  hsmexlem4  10414  hsmexlem5  10415  brdom3  10513  brdom5  10514  brdom4  10515  smobeth  10572  pwfseqlem3  10646  wundm  10714  wunrn  10715  wunex2  10724  ltsopi  10874  dmaddpi  10876  dmmulpi  10877  nqerf  10916  ltrelxr  11271  uzssre  12885  uzwo2  12937  infssuzle  12956  infssuzcl  12957  uzwo3  12968  nn0ssq  12982  nnssq  12983  qsscn  12985  rpnnen1lem3  13004  rpnnen1lem5  13006  dflt2  13174  ioosscn  13436  unitsscn  13528  fzval2  13539  fzossz  13710  fzossnn  13742  injresinj  13822  flval3  13850  uzsup  13898  uzrdgfni  13996  expcl2lem  14111  rpexpcl  14118  expge0  14136  expge1  14137  hashxrcl  14395  seqcoll  14503  xptrrel  15019  trclublem  15034  01sqrexlem3  15297  limsupval2  15533  limsupgre  15534  rlimpm  15553  rlimclim  15599  isercolllem1  15718  isercolllem2  15719  isercoll  15721  caurcvg  15730  caucvg  15732  summolem2a  15768  summolem2  15769  zsum  15771  fsumcvg3  15782  fsumrpcl  15790  fsumge0  15849  climfsum  15874  ackbijnn  15884  prodmolem2a  15990  prodmolem2  15991  zprod  15993  fprodrpcl  16012  fprodge0  16049  fprodge1  16051  rprisefaccl  16079  divalglem8  16459  sadaddlem  16525  lcmfval  16680  isprm3  16742  maxprmfct  16769  pclem  16899  prmreclem1  16977  prmreclem2  16978  prmreclem3  16979  1arith  16988  4sqlem11  17016  ramtlecl  17061  ramcl2lem  17070  ramxrcl  17078  prmgaplem3  17114  prmgaplem4  17115  cshwshashlem1  17156  structfn  17217  strleun  17218  ressbasss  17300  ressbasss2  17302  srngbase  17364  srngplusg  17365  srngmulr  17366  lmodbase  17380  lmodplusg  17381  lmodsca  17382  ipsbase  17391  ipsaddg  17392  ipsmulr  17393  ipssca  17394  ipsvsca  17395  ipsip  17396  phlbase  17401  phlplusg  17402  phlsca  17403  phlvsca  17404  phlip  17405  odrngbas  17458  odrngplusg  17459  odrngmulr  17460  odrngtset  17461  odrngle  17462  odrngds  17463  prdsvallem  17508  prdsval  17509  prdssca  17510  prdsbas  17511  prdsplusg  17512  prdsmulr  17513  prdsvsca  17514  prdsip  17515  prdsle  17516  prdsds  17518  prdstset  17520  prdshom  17521  prdsco  17522  imasbas  17567  imasds  17568  imasplusg  17572  imasmulr  17573  imassca  17574  imasvsca  17575  imasip  17576  imastset  17577  imasle  17578  wunfunc  17959  fullfunc  17966  fthfunc  17967  isfull  17970  isfth  17974  wunnat  18017  dmcoass  18124  catcisolem  18168  catciso  18169  catcoppccl  18175  catcfuccl  18176  catcxpccl  18264  ipobas  18588  ipolerval  18589  ipotset  18590  psdmrn  18630  psss  18637  ledm  18647  lern  18648  dirdm  18657  dirge  18660  mulgfval  19136  mvdco  19516  f1omvdconj  19517  gexex  19924  gsumval3  19978  lssacs  21069  cnfldbas  21507  mpocnfldadd  21508  mpocnfldmul  21510  cnfldcj  21512  cnfldtset  21513  cnfldle  21514  cnfldds  21515  cnfldunif  21516  rge0srg  21569  zntoslem  21687  asplss  22004  aspsubrg  22006  psrass1lem  22064  psrbas  22065  psrplusg  22068  psrmulr  22073  psrsca  22078  psrvscafval  22079  psrass1  22094  psrass23l  22097  psrcom  22098  psrass23  22099  psropprmul  22378  coe1mul2  22411  ofco2  22589  toponsspwpw  23060  dmtopon  23061  leordtval2  23350  lmbrf  23398  lmres  23438  fiuncmp  23542  comppfsc  23670  1stckgenlem  23691  kgencn3  23696  ptbasfi  23719  xkoopn  23727  txcnmpt  23762  txkgen  23790  opnfbas  23980  fmfnfmlem4  24095  tsmsxplem1  24291  trust  24367  restutop  24375  nmoffn  24849  nmofval  24852  nmogelb  24854  nmolb  24855  nmof  24857  qtopbas  24897  tgqioo  24938  re2ndc  24939  iitopon  25019  dfii3  25023  cnheiborlem  25094  bndth  25098  lebnumii  25106  pcoass  25164  cphsqrtcl  25324  lmmbrf  25402  iscauf  25420  caucfil  25423  lmclimf  25444  rrxmval  25545  rrxmet  25548  ovolfioo  25607  ovolficc  25608  ovolficcss  25609  ovolfsf  25611  ovollb  25619  ovolicc2lem3  25659  ovolicc2lem4  25660  ovolicc2  25662  volf  25669  volsup  25696  ovolfs2  25711  uniiccdif  25718  uniioovol  25719  uniiccvol  25720  uniioombllem2  25723  uniioombllem3a  25724  uniioombllem3  25725  uniioombllem4  25726  uniioombllem5  25727  uniioombl  25729  dyadmbllem  25739  dyadmbl  25740  opnmbllem  25741  opnmblALT  25743  volsup2  25745  vitalilem4  25751  vitalilem5  25752  vitali  25753  mbfimaopnlem  25795  mbflimsup  25806  i1f0  25827  i1f1  25830  itg11  25831  itg2mulc  25887  itg2gt0  25900  ellimc2  26017  limcresi  26025  dvreslem  26049  dvres2lem  26050  dvaddbr  26078  dvmulbr  26079  dvlipcn  26134  c1liplem1  26136  lhop1lem  26153  lhop1  26154  lhop2  26155  lhop  26156  dvfsumrlim  26171  ftc1cn  26183  itgsubstlem  26188  itgsubst  26189  itgpowd  26190  mdegleb  26202  mdeglt  26203  mdegldg  26204  mdegxrcl  26205  mdegcl  26207  mdegaddle  26212  mdegmullem  26216  deg1mul3le  26255  ig1peu  26313  ig1pdvds  26318  aacjcl  26471  aannenlem2  26473  aannenlem3  26474  aalioulem2  26477  taylfval  26503  radcnvcl  26561  radcnvlt1  26562  radcnvle  26564  abelth  26585  abelth2  26586  pilem2  26596  pilem3  26597  pige3ALT  26666  recosf1o  26681  resinf1o  26682  tanord1  26683  logcn  26793  dvlog  26797  dvlog2lem  26798  efopn  26804  logtayl  26806  cxpcn3  26894  loglesqrt  26907  ssscongptld  26968  leibpi  27088  efrlim  27115  jensenlem1  27132  jensenlem2  27133  jensen  27134  amgm  27136  lgamgulmlem2  27175  ftalem5  27222  efnnfsumcl  27248  efchtdvds  27304  mpodvdsmulf1o  27339  fsumdvdsmul  27340  dvdsmulf1o  27341  lgsfcl2  27448  2sqlem6  27568  2sqlem8  27571  2sqlem9  27572  rpvmasumlem  27632  rpvmasum2  27657  dchrisum0re  27658  dchrisum0lem3  27664  dchrisum0  27665  rplogsum  27672  dirith2  27673  noextendseq  27812  oldf  28011  leftssno  28047  rightssno  28048  addbdaylem  28191  mulsproplem12  28301  mulsproplem13  28302  mulsproplem14  28303  mulsasslem3  28339  precsexlem11  28391  oncutlt  28438  bdayons  28450  nnssno  28496  axtgcgrrflx  28712  axtgcgrid  28713  axtgsegcon  28714  axtg5seg  28715  axtgbtwnid  28716  axtgpasch  28717  axtgcont1  28718  tgcgr4  28781  motcgrg  28794  tglng  28796  upgrss  29419  pthdivtx  30057  disjxwwlkn  30243  ex-fpar  30794  nmlno0lem  31126  hlimcaui  31569  chsspwh  31580  shsss  31646  chintcli  31664  shsleji  31703  shub1i  31707  shsval2i  31720  lejdii  31871  spanuni  31877  sshhococi  31879  spansnpji  31911  osumcori  31976  5oai  31994  3oalem6  32000  3oai  32001  pjssmii  32014  mayete3i  32061  mayetes3i  32062  nmlnop0iALT  32328  imaelshi  32391  pjnmopi  32481  pjclem1  32528  pjci  32533  mdslmd1lem1  32658  shatomistici  32694  hatomistici  32695  chpssati  32696  xppreima  32971  iundisjfi  33122  iundisj2fi  33123  fprodex01  33150  indsumin  33162  xrsmulgzz  33310  fsumrp0cl  33322  gsummpt2co  33349  cycpmfv2  33415  cycpmrn  33444  rlocbas  33569  rlocaddval  33570  rlocmulval  33571  1fldgenq  33624  xrge0slmod  33649  lsmsnorb  33685  idlsrgbas  33775  idlsrgplusg  33776  idlsrgmulr  33778  idlsrgtset  33779  selvply1rhmlemb  33890  esplyind  33946  vietalem  33950  constrextdg2  34120  ordtconnlem1  34295  xrge0iifhom  34308  lmlimxrge0  34319  lmxrge0  34323  esumcst  34434  esumpfinvallem  34445  esumpfinval  34446  esumpfinvalf  34447  esumcvg  34457  imambfm  34633  elmbfmvol2  34638  sxbrsigalem3  34643  sxbrsigalem2  34657  sxbrsigalem4  34658  sitgclg  34713  eulerpartlem1  34738  eulerpartlemgvv  34747  eulerpartlemgh  34749  eulerpartlemgf  34750  ballotlemfc0  34864  ballotlemfcc  34865  ballotlemiex  34873  ballotlemsup  34876  ballotlemsima  34887  ballotlemrv2  34893  ballotth  34909  signsplypnf  34918  signsply0  34919  rpsqrtcn  34961  itgexpif  34974  fsum2dsub  34975  reprfi2  34991  chtvalz  34997  breprexplemc  35000  breprexpnat  35002  circlemeth  35008  circlemethnat  35009  circlevma  35010  circlemethhgt  35011  hgt750lemd  35016  hgt750lema  35025  tgoldbachgtde  35028  tgoldbachgtda  35029  tgoldbachgt  35031  bnj1145  35362  bnj1286  35388  subfacp1lem2a  35653  erdszelem4  35667  erdszelem5  35668  erdszelem7  35670  erdszelem8  35671  kur14lem7  35685  kur14lem9  35687  resconn  35719  iccllysconn  35723  txpss3v  36349  txprel  36350  limitssson  36382  finminlem  36810  tailf  36867  filnetlem3  36872  onint1  36941  ttcuniun  37002  bj-unrab  37543  bj-2upln1upl  37641  bj-imdirco  37815  bj-rvecssabl  37931  taupilem2  37947  taupi  37948  poimirlem3  38255  poimirlem30  38282  poimirlem31  38283  poimirlem32  38284  broucube  38286  opnmbllem0  38288  mblfinlem1  38289  mblfinlem2  38290  mblfinlem3  38291  mblfinlem4  38292  ismblfin  38293  mbfposadd  38299  cnambfre  38300  itg2addnc  38306  ftc1cnnclem  38323  ftc1cnnc  38324  ftc1anclem3  38327  ftc1anclem7  38331  ftc1anc  38333  ftc2nc  38334  dvreasin  38338  dvreacos  38339  areacirclem1  38340  areacirclem2  38341  areacirc  38345  caures  38392  reheibor  38471  xrnss3v  39011  xrnrel  39012  atlatmstc  40074  atlatle  40075  pmaple  40516  sspadd1  40570  sspadd2  40571  dvrelog2  42812  dvrelog3  42813  rpsscn  43041  sumcubes  43055  redvmptabs  43102  diophin  43486  4rexfrabdioph  43508  6rexfrabdioph  43509  irrapxlem1  43532  irrapx1  43538  rmxyelqirr  43620  monotuz  43651  jm2.27dlem5  43723  hbtlem2  43834  algbase  43884  algaddg  43885  algmulr  43886  algsca  43887  algvsca  43888  arearect  43925  areaquad  43926  rtrclex  44326  trclubgNEW  44327  trclexi  44329  rtrclexi  44330  cnvtrcl0  44335  dfrtrcl5  44338  trrelsuperrel2dg  44380  relexpaddss  44427  brtrclfv2  44436  frege131d  44473  xphe  44490  clsk3nimkb  44749  gneispace  44843  k0004val0  44863  inaex  44990  lhe4.4ex1a  45022  uzmptshftfval  45039  binomcxplemdvbinom  45046  binomcxplemcvg  45047  binomcxplemnotnn0  45049  relopabVD  45592  dmwf  45657  rnwf  45658  fzisoeu  46002  fzsscn  46013  fzssre  46016  fzossuz  46079  zssxr  46095  uzssre2  46104  supminfxr  46161  uzsscn  46172  rpssxr  46177  uzinico  46258  limcresiooub  46339  limcresioolb  46340  limcleqr  46341  limclner  46348  limclr  46352  limsupequzmpt2  46415  liminfval2  46465  liminfequzmpt2  46488  icccncfext  46584  cncficcgt0  46585  ioodvbdlimc1lem2  46629  ioodvbdlimc2lem  46631  dvnprodlem2  46644  itgsin0pilem1  46647  itgsinexplem1  46651  itgsinexp  46652  dirkercncflem2  46801  fourierdlem16  46820  fourierdlem18  46822  fourierdlem20  46824  fourierdlem21  46825  fourierdlem22  46826  fourierdlem25  46829  fourierdlem37  46841  fourierdlem42  46846  fourierdlem50  46853  fourierdlem52  46855  fourierdlem62  46865  fourierdlem64  46867  fourierdlem66  46869  fourierdlem68  46871  fourierdlem74  46877  fourierdlem75  46878  fourierdlem76  46879  fourierdlem79  46882  fourierdlem83  46886  fourierdlem95  46898  fourierdlem101  46904  fourierdlem102  46905  fourierdlem103  46906  fourierdlem104  46907  fourierdlem112  46915  fourierdlem114  46917  sqwvfoura  46925  sqwvfourb  46926  fouriersw  46928  etransclem24  46955  etransclem48  46979  sge0sn  47076  sge0tsms  47077  sge0f1o  47079  sge0pr  47091  sge0resplit  47103  sge0split  47106  sge0iunmptlemre  47112  sge0isummpt2  47129  carageniuncllem1  47218  hoicvr  47245  hoicvrrex  47253  hoidmvlelem2  47293  hspmbl  47326  smfmullem4  47491  chnsuslle  47580  lamberte  47608  rehalfge1  48059  prmdvdsfmtnof1lem1  48319  prmdvdsfmtnof  48321  upgrimpthslem2  48656  upgrimpths  48657  oddibas  48921  2zrngbas  48990  2zrng0  48992  dmtposss  49637  tposres3  49642  sepfsepc  49689  uptrlem1  49971  uptrlem2  49972  uptrlem3  49973  uptra  49976  uptrar  49977  uobeqw  49980  uptr2  49982  uptr2a  49983  fucoppcfunc  50173  aacllem  50584  amgmlemALT  50586