Theorem sstri 3993

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

Syntax hints:   ⊆ wss 3951

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 3968

This theorem is referenced by:  snsstp1  4816  snsstp2  4817  uniintsn  4985  elopabran  5567  ssrnres  6198  cossxp  6292  foimacnv  6865  ssimaex  6994  riotassuni  7428  oprabss  7541  dmexg  7923  rnexg  7924  fabexgOLD  7961  mptmpoopabbrd  8105  fparlem3  8139  fparlem4  8140  snopsuppss  8204  tposssxp  8255  naddunif  8731  naddasslem1  8732  naddasslem2  8733  mapsspw  8918  sbthlem5  9127  sbthlem7  9129  cnvimamptfin  9393  marypha1lem  9473  ordtypelem4  9561  hartogslem1  9582  ttrclco  9758  cottrcl  9759  tc2  9782  frmin  9789  frrlem16  9798  tz9.12lem1  9827  rankval4  9907  rankxpl  9915  rankmapu  9918  rankxplim  9919  djuin  9958  infxpenlem  10053  ackbij1lem18  10276  cflm  10290  fin23lem29  10381  hsmexlem4  10469  hsmexlem5  10470  brdom3  10568  brdom5  10569  brdom4  10570  smobeth  10626  pwfseqlem3  10700  wundm  10768  wunrn  10769  wunex2  10778  ltsopi  10928  dmaddpi  10930  dmmulpi  10931  nqerf  10970  ltrelxr  11322  uzssre  12900  uzwo2  12954  infssuzle  12973  infssuzcl  12974  uzwo3  12985  nn0ssq  12999  nnssq  13000  qsscn  13002  rpnnen1lem3  13021  rpnnen1lem5  13023  dflt2  13190  ioosscn  13449  unitsscn  13540  fzval2  13550  fzossz  13719  fzossnn  13751  injresinj  13827  flval3  13855  uzsup  13903  uzrdgfni  13999  expcl2lem  14114  rpexpcl  14121  expge0  14139  expge1  14140  hashxrcl  14396  seqcoll  14503  xptrrel  15019  trclublem  15034  01sqrexlem3  15283  limsupval2  15516  limsupgre  15517  rlimpm  15536  rlimclim  15582  isercolllem1  15701  isercolllem2  15702  isercoll  15704  caurcvg  15713  caucvg  15715  summolem2a  15751  summolem2  15752  zsum  15754  fsumcvg3  15765  fsumrpcl  15773  fsumge0  15831  climfsum  15856  ackbijnn  15864  prodmolem2a  15970  prodmolem2  15971  zprod  15973  fprodrpcl  15992  fprodge0  16029  fprodge1  16031  rprisefaccl  16059  divalglem8  16437  sadaddlem  16503  lcmfval  16658  isprm3  16720  maxprmfct  16746  pclem  16876  prmreclem1  16954  prmreclem2  16955  prmreclem3  16956  1arith  16965  4sqlem11  16993  ramtlecl  17038  ramcl2lem  17047  ramxrcl  17055  prmgaplem3  17091  prmgaplem4  17092  cshwshashlem1  17133  structfn  17193  strleun  17194  ressbasss  17284  ressbasss2  17286  srngbase  17354  srngplusg  17355  srngmulr  17356  lmodbase  17370  lmodplusg  17371  lmodsca  17372  ipsbase  17381  ipsaddg  17382  ipsmulr  17383  ipssca  17384  ipsvsca  17385  ipsip  17386  phlbase  17391  phlplusg  17392  phlsca  17393  phlvsca  17394  phlip  17395  odrngbas  17448  odrngplusg  17449  odrngmulr  17450  odrngtset  17451  odrngle  17452  odrngds  17453  prdsvallem  17499  prdsval  17500  prdssca  17501  prdsbas  17502  prdsplusg  17503  prdsmulr  17504  prdsvsca  17505  prdsip  17506  prdsle  17507  prdsds  17509  prdstset  17511  prdshom  17512  prdsco  17513  imasbas  17557  imasds  17558  imasplusg  17562  imasmulr  17563  imassca  17564  imasvsca  17565  imasip  17566  imastset  17567  imasle  17568  wunfunc  17946  fullfunc  17953  fthfunc  17954  isfull  17957  isfth  17961  wunnat  18004  dmcoass  18111  catcisolem  18155  catciso  18156  catcoppccl  18162  catcfuccl  18163  catcxpccl  18252  ipobas  18576  ipolerval  18577  ipotset  18578  psdmrn  18618  psss  18625  ledm  18635  lern  18636  dirdm  18645  dirge  18648  mulgfval  19087  mvdco  19463  f1omvdconj  19464  gexex  19871  gsumval3  19925  lssacs  20965  cnfldbas  21368  mpocnfldadd  21369  mpocnfldmul  21371  cnfldcj  21373  cnfldtset  21374  cnfldle  21375  cnfldds  21376  cnfldunif  21377  cnfldbasOLD  21383  cnfldaddOLD  21384  cnfldmulOLD  21385  cnfldcjOLD  21386  cnfldtsetOLD  21387  cnfldleOLD  21388  cnflddsOLD  21389  cnfldunifOLD  21390  rge0srg  21456  zntoslem  21575  asplss  21894  aspsubrg  21896  psrass1lem  21952  psrbas  21953  psrplusg  21956  psrmulr  21962  psrsca  21967  psrvscafval  21968  psrass1  21984  psrass23l  21987  psrcom  21988  psrass23  21989  psropprmul  22239  coe1mul2  22272  ofco2  22457  toponsspwpw  22928  dmtopon  22929  leordtval2  23220  lmbrf  23268  lmres  23308  fiuncmp  23412  comppfsc  23540  1stckgenlem  23561  kgencn3  23566  ptbasfi  23589  xkoopn  23597  txcnmpt  23632  txkgen  23660  opnfbas  23850  fmfnfmlem4  23965  tsmsxplem1  24161  trust  24238  restutop  24246  nmoffn  24732  nmofval  24735  nmogelb  24737  nmolb  24738  nmof  24740  qtopbas  24780  tgqioo  24821  re2ndc  24822  iitopon  24905  dfii3  24909  iimulcnOLD  24968  cnheiborlem  24986  bndth  24990  lebnumii  24998  reparphtiOLD  25030  pcoass  25057  cphsqrtcl  25218  lmmbrf  25296  iscauf  25314  caucfil  25317  lmclimf  25338  rrxmval  25439  rrxmet  25442  ovolfioo  25502  ovolficc  25503  ovolficcss  25504  ovolfsf  25506  ovollb  25514  ovolicc2lem3  25554  ovolicc2lem4  25555  ovolicc2  25557  volf  25564  volsup  25591  ovolfs2  25606  uniiccdif  25613  uniioovol  25614  uniiccvol  25615  uniioombllem2  25618  uniioombllem3a  25619  uniioombllem3  25620  uniioombllem4  25621  uniioombllem5  25622  uniioombl  25624  dyadmbllem  25634  dyadmbl  25635  opnmbllem  25636  opnmblALT  25638  volsup2  25640  vitalilem4  25646  vitalilem5  25647  vitali  25648  mbfimaopnlem  25690  mbflimsup  25701  i1f0  25722  i1f1  25725  itg11  25726  itg2mulc  25782  itg2gt0  25795  ellimc2  25912  limcresi  25920  dvreslem  25944  dvres2lem  25945  dvaddbr  25974  dvmulbr  25975  dvmulbrOLD  25976  dvlipcn  26033  c1liplem1  26035  lhop1lem  26052  lhop1  26053  lhop2  26054  lhop  26055  dvfsumrlim  26072  ftc1cn  26084  itgsubstlem  26089  itgsubst  26090  itgpowd  26091  mdegleb  26103  mdeglt  26104  mdegldg  26105  mdegxrcl  26106  mdegcl  26108  mdegaddle  26113  mdegmullem  26117  deg1mul3le  26156  ig1peu  26214  ig1pdvds  26219  aacjcl  26369  aannenlem2  26371  aannenlem3  26372  aalioulem2  26375  taylfval  26400  radcnvcl  26460  radcnvlt1  26461  radcnvle  26463  abelth  26485  abelth2  26486  pilem2  26496  pilem3  26497  pige3ALT  26562  recosf1o  26577  resinf1o  26578  tanord1  26579  logcn  26689  dvlog  26693  dvlog2lem  26694  efopn  26700  logtayl  26702  cxpcn3  26791  loglesqrt  26804  ssscongptld  26865  leibpi  26985  efrlim  27012  efrlimOLD  27013  jensenlem1  27030  jensenlem2  27031  jensen  27032  amgm  27034  lgamgulmlem2  27073  ftalem5  27120  efnnfsumcl  27146  efchtdvds  27202  mpodvdsmulf1o  27237  fsumdvdsmul  27238  dvdsmulf1o  27239  fsumdvdsmulOLD  27240  lgsfcl2  27347  2sqlem6  27467  2sqlem8  27470  2sqlem9  27471  rpvmasumlem  27531  rpvmasum2  27556  dchrisum0re  27557  dchrisum0lem3  27563  dchrisum0  27564  rplogsum  27571  dirith2  27572  noextendseq  27712  oldf  27896  leftssno  27919  rightssno  27920  addsbdaylem  28049  mulsproplem12  28153  mulsproplem13  28154  mulsproplem14  28155  mulsasslem3  28191  precsexlem11  28241  nnssno  28327  axtgcgrrflx  28470  axtgcgrid  28471  axtgsegcon  28472  axtg5seg  28473  axtgbtwnid  28474  axtgpasch  28475  axtgcont1  28476  tgcgr4  28539  motcgrg  28552  tglng  28554  upgrss  29105  pthdivtx  29747  disjxwwlkn  29933  ex-fpar  30481  nmlno0lem  30812  hlimcaui  31255  chsspwh  31266  shsss  31332  chintcli  31350  shsleji  31389  shub1i  31393  shsval2i  31406  lejdii  31557  spanuni  31563  sshhococi  31565  spansnpji  31597  osumcori  31662  5oai  31680  3oalem6  31686  3oai  31687  pjssmii  31700  mayete3i  31747  mayetes3i  31748  nmlnop0iALT  32014  imaelshi  32077  pjnmopi  32167  pjclem1  32214  pjci  32219  mdslmd1lem1  32344  shatomistici  32380  hatomistici  32381  chpssati  32382  xppreima  32655  iundisjfi  32798  iundisj2fi  32799  fprodex01  32827  indsumin  32847  xrsmulgzz  33011  fsumrp0cl  33026  gsummpt2co  33051  cycpmfv2  33134  cycpmrn  33163  rlocbas  33271  rlocaddval  33272  rlocmulval  33273  1fldgenq  33324  xrge0slmod  33376  lsmsnorb  33419  idlsrgbas  33532  idlsrgplusg  33533  idlsrgmulr  33535  idlsrgtset  33536  constrextdg2  33790  ordtconnlem1  33923  xrge0iifhom  33936  lmlimxrge0  33947  lmxrge0  33951  esumcst  34064  esumpfinvallem  34075  esumpfinval  34076  esumpfinvalf  34077  esumcvg  34087  imambfm  34264  elmbfmvol2  34269  sxbrsigalem3  34274  sxbrsigalem2  34288  sxbrsigalem4  34289  sitgclg  34344  eulerpartlem1  34369  eulerpartlemgvv  34378  eulerpartlemgh  34380  eulerpartlemgf  34381  ballotlemfc0  34495  ballotlemfcc  34496  ballotlemiex  34504  ballotlemsup  34507  ballotlemsima  34518  ballotlemrv2  34524  ballotth  34540  signsplypnf  34565  signsply0  34566  rpsqrtcn  34608  itgexpif  34621  fsum2dsub  34622  reprfi2  34638  chtvalz  34644  breprexplemc  34647  breprexpnat  34649  circlemeth  34655  circlemethnat  34656  circlevma  34657  circlemethhgt  34658  hgt750lemd  34663  hgt750lema  34672  tgoldbachgtde  34675  tgoldbachgtda  34676  tgoldbachgt  34678  bnj1145  35007  bnj1286  35033  subfacp1lem2a  35185  erdszelem4  35199  erdszelem5  35200  erdszelem7  35202  erdszelem8  35203  kur14lem7  35217  kur14lem9  35219  resconn  35251  iccllysconn  35255  txpss3v  35879  txprel  35880  limitssson  35912  finminlem  36319  tailf  36376  filnetlem3  36381  onint1  36450  bj-unrab  36927  bj-2upln1upl  37025  bj-imdirco  37191  bj-rvecssabl  37307  taupilem2  37323  taupi  37324  poimirlem3  37630  poimirlem30  37657  poimirlem31  37658  poimirlem32  37659  broucube  37661  opnmbllem0  37663  mblfinlem1  37664  mblfinlem2  37665  mblfinlem3  37666  mblfinlem4  37667  ismblfin  37668  mbfposadd  37674  cnambfre  37675  itg2addnc  37681  ftc1cnnclem  37698  ftc1cnnc  37699  ftc1anclem3  37702  ftc1anclem7  37706  ftc1anc  37708  ftc2nc  37709  dvreasin  37713  dvreacos  37714  areacirclem1  37715  areacirclem2  37716  areacirc  37720  caures  37767  reheibor  37846  xrnss3v  38373  xrnrel  38374  atlatmstc  39320  atlatle  39321  pmaple  39763  sspadd1  39817  sspadd2  39818  dvrelog2  42065  dvrelog3  42066  rpsscn  42333  sumcubes  42347  redvmptabs  42390  diophin  42783  4rexfrabdioph  42809  6rexfrabdioph  42810  irrapxlem1  42833  irrapx1  42839  rmxyelqirr  42921  monotuz  42953  jm2.27dlem5  43025  hbtlem2  43136  algbase  43186  algaddg  43187  algmulr  43188  algsca  43189  algvsca  43190  arearect  43227  areaquad  43228  rtrclex  43630  trclubgNEW  43631  trclexi  43633  rtrclexi  43634  cnvtrcl0  43639  dfrtrcl5  43642  trrelsuperrel2dg  43684  relexpaddss  43731  brtrclfv2  43740  frege131d  43777  xphe  43794  clsk3nimkb  44053  gneispace  44147  k0004val0  44167  inaex  44316  lhe4.4ex1a  44348  uzmptshftfval  44365  binomcxplemdvbinom  44372  binomcxplemcvg  44373  binomcxplemnotnn0  44375  relopabVD  44921  dmwf  44982  rnwf  44983  fzisoeu  45312  fzsscn  45323  fzssre  45326  fzossuz  45392  zssxr  45408  uzssre2  45418  supminfxr  45475  uzsscn  45486  rpssxr  45491  uzinico  45573  limcresiooub  45657  limcresioolb  45658  limcleqr  45659  limclner  45666  limclr  45670  limsupequzmpt2  45733  liminfval2  45783  liminfequzmpt2  45806  icccncfext  45902  cncficcgt0  45903  ioodvbdlimc1lem2  45947  ioodvbdlimc2lem  45949  dvnprodlem2  45962  itgsin0pilem1  45965  itgsinexplem1  45969  itgsinexp  45970  dirkercncflem2  46119  fourierdlem16  46138  fourierdlem18  46140  fourierdlem20  46142  fourierdlem21  46143  fourierdlem22  46144  fourierdlem25  46147  fourierdlem37  46159  fourierdlem42  46164  fourierdlem50  46171  fourierdlem52  46173  fourierdlem62  46183  fourierdlem64  46185  fourierdlem66  46187  fourierdlem68  46189  fourierdlem74  46195  fourierdlem75  46196  fourierdlem76  46197  fourierdlem79  46200  fourierdlem83  46204  fourierdlem95  46216  fourierdlem101  46222  fourierdlem102  46223  fourierdlem103  46224  fourierdlem104  46225  fourierdlem112  46233  fourierdlem114  46235  sqwvfoura  46243  sqwvfourb  46244  fouriersw  46246  etransclem24  46273  etransclem48  46297  sge0sn  46394  sge0tsms  46395  sge0f1o  46397  sge0pr  46409  sge0resplit  46421  sge0split  46424  sge0iunmptlemre  46430  sge0isummpt2  46447  carageniuncllem1  46536  hoicvr  46563  hoicvrrex  46571  hoidmvlelem2  46611  hspmbl  46644  smfmullem4  46809  prmdvdsfmtnof1lem1  47571  prmdvdsfmtnof  47573  oddibas  48089  2zrngbas  48158  2zrng0  48160  dmtposss  48776  tposres3  48781  sepfsepc  48825  aacllem  49320  amgmlemALT  49322