Theorem sstri 3945

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

Syntax hints:   ⊆ wss 3903

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

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

This theorem is referenced by:  snsstp1  4774  snsstp2  4775  uniintsn  4942  elopabran  5517  ssrnres  6144  cossxp  6238  foimacnv  6799  ssimaex  6927  riotassuni  7365  oprabss  7476  dmexg  7853  rnexg  7854  fabexgOLD  7891  mptmpoopabbrd  8034  fparlem3  8066  fparlem4  8067  snopsuppss  8131  tposssxp  8182  naddunif  8631  naddasslem1  8632  naddasslem2  8633  mapsspw  8828  sbthlem5  9031  sbthlem7  9033  cnvimamptfin  9265  marypha1lem  9348  ordtypelem4  9438  hartogslem1  9459  ttrclco  9639  cottrcl  9640  tc2  9661  frmin  9673  frrlem16  9682  tz9.12lem1  9711  rankval4  9791  rankxpl  9799  rankmapu  9802  rankxplim  9803  djuin  9842  infxpenlem  9935  ackbij1lem18  10158  cflm  10172  fin23lem29  10263  hsmexlem4  10351  hsmexlem5  10352  brdom3  10450  brdom5  10451  brdom4  10452  smobeth  10509  pwfseqlem3  10583  wundm  10651  wunrn  10652  wunex2  10661  ltsopi  10811  dmaddpi  10813  dmmulpi  10814  nqerf  10853  ltrelxr  11205  uzssre  12785  uzwo2  12837  infssuzle  12856  infssuzcl  12857  uzwo3  12868  nn0ssq  12882  nnssq  12883  qsscn  12885  rpnnen1lem3  12904  rpnnen1lem5  12906  dflt2  13074  ioosscn  13336  unitsscn  13428  fzval2  13438  fzossz  13607  fzossnn  13639  injresinj  13719  flval3  13747  uzsup  13795  uzrdgfni  13893  expcl2lem  14008  rpexpcl  14015  expge0  14033  expge1  14034  hashxrcl  14292  seqcoll  14399  xptrrel  14915  trclublem  14930  01sqrexlem3  15179  limsupval2  15415  limsupgre  15416  rlimpm  15435  rlimclim  15481  isercolllem1  15600  isercolllem2  15601  isercoll  15603  caurcvg  15612  caucvg  15614  summolem2a  15650  summolem2  15651  zsum  15653  fsumcvg3  15664  fsumrpcl  15672  fsumge0  15730  climfsum  15755  ackbijnn  15763  prodmolem2a  15869  prodmolem2  15870  zprod  15872  fprodrpcl  15891  fprodge0  15928  fprodge1  15930  rprisefaccl  15958  divalglem8  16339  sadaddlem  16405  lcmfval  16560  isprm3  16622  maxprmfct  16648  pclem  16778  prmreclem1  16856  prmreclem2  16857  prmreclem3  16858  1arith  16867  4sqlem11  16895  ramtlecl  16940  ramcl2lem  16949  ramxrcl  16957  prmgaplem3  16993  prmgaplem4  16994  cshwshashlem1  17035  structfn  17095  strleun  17096  ressbasss  17178  ressbasss2  17180  srngbase  17242  srngplusg  17243  srngmulr  17244  lmodbase  17258  lmodplusg  17259  lmodsca  17260  ipsbase  17269  ipsaddg  17270  ipsmulr  17271  ipssca  17272  ipsvsca  17273  ipsip  17274  phlbase  17279  phlplusg  17280  phlsca  17281  phlvsca  17282  phlip  17283  odrngbas  17336  odrngplusg  17337  odrngmulr  17338  odrngtset  17339  odrngle  17340  odrngds  17341  prdsvallem  17386  prdsval  17387  prdssca  17388  prdsbas  17389  prdsplusg  17390  prdsmulr  17391  prdsvsca  17392  prdsip  17393  prdsle  17394  prdsds  17396  prdstset  17398  prdshom  17399  prdsco  17400  imasbas  17445  imasds  17446  imasplusg  17450  imasmulr  17451  imassca  17452  imasvsca  17453  imasip  17454  imastset  17455  imasle  17456  wunfunc  17837  fullfunc  17844  fthfunc  17845  isfull  17848  isfth  17852  wunnat  17895  dmcoass  18002  catcisolem  18046  catciso  18047  catcoppccl  18053  catcfuccl  18054  catcxpccl  18142  ipobas  18466  ipolerval  18467  ipotset  18468  psdmrn  18508  psss  18515  ledm  18525  lern  18526  dirdm  18535  dirge  18538  mulgfval  19011  mvdco  19386  f1omvdconj  19387  gexex  19794  gsumval3  19848  lssacs  20930  cnfldbas  21325  mpocnfldadd  21326  mpocnfldmul  21328  cnfldcj  21330  cnfldtset  21331  cnfldle  21332  cnfldds  21333  cnfldunif  21334  cnfldbasOLD  21340  cnfldaddOLD  21341  cnfldmulOLD  21342  cnfldcjOLD  21343  cnfldtsetOLD  21344  cnfldleOLD  21345  cnflddsOLD  21346  cnfldunifOLD  21347  rge0srg  21405  zntoslem  21523  asplss  21841  aspsubrg  21843  psrass1lem  21900  psrbas  21901  psrplusg  21904  psrmulr  21910  psrsca  21915  psrvscafval  21916  psrass1  21931  psrass23l  21934  psrcom  21935  psrass23  21936  psropprmul  22190  coe1mul2  22223  ofco2  22407  toponsspwpw  22878  dmtopon  22879  leordtval2  23168  lmbrf  23216  lmres  23256  fiuncmp  23360  comppfsc  23488  1stckgenlem  23509  kgencn3  23514  ptbasfi  23537  xkoopn  23545  txcnmpt  23580  txkgen  23608  opnfbas  23798  fmfnfmlem4  23913  tsmsxplem1  24109  trust  24185  restutop  24193  nmoffn  24667  nmofval  24670  nmogelb  24672  nmolb  24673  nmof  24675  qtopbas  24715  tgqioo  24756  re2ndc  24757  iitopon  24840  dfii3  24844  iimulcnOLD  24903  cnheiborlem  24921  bndth  24925  lebnumii  24933  reparphtiOLD  24965  pcoass  24992  cphsqrtcl  25152  lmmbrf  25230  iscauf  25248  caucfil  25251  lmclimf  25272  rrxmval  25373  rrxmet  25376  ovolfioo  25436  ovolficc  25437  ovolficcss  25438  ovolfsf  25440  ovollb  25448  ovolicc2lem3  25488  ovolicc2lem4  25489  ovolicc2  25491  volf  25498  volsup  25525  ovolfs2  25540  uniiccdif  25547  uniioovol  25548  uniiccvol  25549  uniioombllem2  25552  uniioombllem3a  25553  uniioombllem3  25554  uniioombllem4  25555  uniioombllem5  25556  uniioombl  25558  dyadmbllem  25568  dyadmbl  25569  opnmbllem  25570  opnmblALT  25572  volsup2  25574  vitalilem4  25580  vitalilem5  25581  vitali  25582  mbfimaopnlem  25624  mbflimsup  25635  i1f0  25656  i1f1  25659  itg11  25660  itg2mulc  25716  itg2gt0  25729  ellimc2  25846  limcresi  25854  dvreslem  25878  dvres2lem  25879  dvaddbr  25908  dvmulbr  25909  dvmulbrOLD  25910  dvlipcn  25967  c1liplem1  25969  lhop1lem  25986  lhop1  25987  lhop2  25988  lhop  25989  dvfsumrlim  26006  ftc1cn  26018  itgsubstlem  26023  itgsubst  26024  itgpowd  26025  mdegleb  26037  mdeglt  26038  mdegldg  26039  mdegxrcl  26040  mdegcl  26042  mdegaddle  26047  mdegmullem  26051  deg1mul3le  26090  ig1peu  26148  ig1pdvds  26153  aacjcl  26303  aannenlem2  26305  aannenlem3  26306  aalioulem2  26309  taylfval  26334  radcnvcl  26394  radcnvlt1  26395  radcnvle  26397  abelth  26419  abelth2  26420  pilem2  26430  pilem3  26431  pige3ALT  26497  recosf1o  26512  resinf1o  26513  tanord1  26514  logcn  26624  dvlog  26628  dvlog2lem  26629  efopn  26635  logtayl  26637  cxpcn3  26726  loglesqrt  26739  ssscongptld  26800  leibpi  26920  efrlim  26947  efrlimOLD  26948  jensenlem1  26965  jensenlem2  26966  jensen  26967  amgm  26969  lgamgulmlem2  27008  ftalem5  27055  efnnfsumcl  27081  efchtdvds  27137  mpodvdsmulf1o  27172  fsumdvdsmul  27173  dvdsmulf1o  27174  fsumdvdsmulOLD  27175  lgsfcl2  27282  2sqlem6  27402  2sqlem8  27405  2sqlem9  27406  rpvmasumlem  27466  rpvmasum2  27491  dchrisum0re  27492  dchrisum0lem3  27498  dchrisum0  27499  rplogsum  27506  dirith2  27507  noextendseq  27647  oldf  27845  leftssno  27881  rightssno  27882  addbdaylem  28025  mulsproplem12  28135  mulsproplem13  28136  mulsproplem14  28137  mulsasslem3  28173  precsexlem11  28225  oncutlt  28272  bdayons  28284  nnssno  28330  axtgcgrrflx  28546  axtgcgrid  28547  axtgsegcon  28548  axtg5seg  28549  axtgbtwnid  28550  axtgpasch  28551  axtgcont1  28552  tgcgr4  28615  motcgrg  28628  tglng  28630  upgrss  29173  pthdivtx  29812  disjxwwlkn  29998  ex-fpar  30549  nmlno0lem  30880  hlimcaui  31323  chsspwh  31334  shsss  31400  chintcli  31418  shsleji  31457  shub1i  31461  shsval2i  31474  lejdii  31625  spanuni  31631  sshhococi  31633  spansnpji  31665  osumcori  31730  5oai  31748  3oalem6  31754  3oai  31755  pjssmii  31768  mayete3i  31815  mayetes3i  31816  nmlnop0iALT  32082  imaelshi  32145  pjnmopi  32235  pjclem1  32282  pjci  32287  mdslmd1lem1  32412  shatomistici  32448  hatomistici  32449  chpssati  32450  xppreima  32734  iundisjfi  32886  iundisj2fi  32887  fprodex01  32916  indsumin  32953  xrsmulgzz  33101  fsumrp0cl  33113  gsummpt2co  33141  cycpmfv2  33207  cycpmrn  33236  rlocbas  33360  rlocaddval  33361  rlocmulval  33362  1fldgenq  33415  xrge0slmod  33440  lsmsnorb  33483  idlsrgbas  33596  idlsrgplusg  33597  idlsrgmulr  33599  idlsrgtset  33600  esplyind  33751  vietalem  33755  constrextdg2  33926  ordtconnlem1  34101  xrge0iifhom  34114  lmlimxrge0  34125  lmxrge0  34129  esumcst  34240  esumpfinvallem  34251  esumpfinval  34252  esumpfinvalf  34253  esumcvg  34263  imambfm  34439  elmbfmvol2  34444  sxbrsigalem3  34449  sxbrsigalem2  34463  sxbrsigalem4  34464  sitgclg  34519  eulerpartlem1  34544  eulerpartlemgvv  34553  eulerpartlemgh  34555  eulerpartlemgf  34556  ballotlemfc0  34670  ballotlemfcc  34671  ballotlemiex  34679  ballotlemsup  34682  ballotlemsima  34693  ballotlemrv2  34699  ballotth  34715  signsplypnf  34727  signsply0  34728  rpsqrtcn  34770  itgexpif  34783  fsum2dsub  34784  reprfi2  34800  chtvalz  34806  breprexplemc  34809  breprexpnat  34811  circlemeth  34817  circlemethnat  34818  circlevma  34819  circlemethhgt  34820  hgt750lemd  34825  hgt750lema  34834  tgoldbachgtde  34837  tgoldbachgtda  34838  tgoldbachgt  34840  bnj1145  35168  bnj1286  35194  subfacp1lem2a  35393  erdszelem4  35407  erdszelem5  35408  erdszelem7  35410  erdszelem8  35411  kur14lem7  35425  kur14lem9  35427  resconn  35459  iccllysconn  35463  txpss3v  36089  txprel  36090  limitssson  36122  finminlem  36531  tailf  36588  filnetlem3  36593  onint1  36662  bj-unrab  37171  bj-2upln1upl  37269  bj-imdirco  37442  bj-rvecssabl  37558  taupilem2  37574  taupi  37575  poimirlem3  37871  poimirlem30  37898  poimirlem31  37899  poimirlem32  37900  broucube  37902  opnmbllem0  37904  mblfinlem1  37905  mblfinlem2  37906  mblfinlem3  37907  mblfinlem4  37908  ismblfin  37909  mbfposadd  37915  cnambfre  37916  itg2addnc  37922  ftc1cnnclem  37939  ftc1cnnc  37940  ftc1anclem3  37943  ftc1anclem7  37947  ftc1anc  37949  ftc2nc  37950  dvreasin  37954  dvreacos  37955  areacirclem1  37956  areacirclem2  37957  areacirc  37961  caures  38008  reheibor  38087  xrnss3v  38629  xrnrel  38630  atlatmstc  39692  atlatle  39693  pmaple  40134  sspadd1  40188  sspadd2  40189  dvrelog2  42431  dvrelog3  42432  rpsscn  42666  sumcubes  42680  redvmptabs  42727  diophin  43126  4rexfrabdioph  43152  6rexfrabdioph  43153  irrapxlem1  43176  irrapx1  43182  rmxyelqirr  43264  monotuz  43295  jm2.27dlem5  43367  hbtlem2  43478  algbase  43528  algaddg  43529  algmulr  43530  algsca  43531  algvsca  43532  arearect  43569  areaquad  43570  rtrclex  43970  trclubgNEW  43971  trclexi  43973  rtrclexi  43974  cnvtrcl0  43979  dfrtrcl5  43982  trrelsuperrel2dg  44024  relexpaddss  44071  brtrclfv2  44080  frege131d  44117  xphe  44134  clsk3nimkb  44393  gneispace  44487  k0004val0  44507  inaex  44650  lhe4.4ex1a  44682  uzmptshftfval  44699  binomcxplemdvbinom  44706  binomcxplemcvg  44707  binomcxplemnotnn0  44709  relopabVD  45253  dmwf  45318  rnwf  45319  fzisoeu  45659  fzsscn  45670  fzssre  45673  fzossuz  45736  zssxr  45752  uzssre2  45762  supminfxr  45819  uzsscn  45830  rpssxr  45835  uzinico  45916  limcresiooub  45997  limcresioolb  45998  limcleqr  45999  limclner  46006  limclr  46010  limsupequzmpt2  46073  liminfval2  46123  liminfequzmpt2  46146  icccncfext  46242  cncficcgt0  46243  ioodvbdlimc1lem2  46287  ioodvbdlimc2lem  46289  dvnprodlem2  46302  itgsin0pilem1  46305  itgsinexplem1  46309  itgsinexp  46310  dirkercncflem2  46459  fourierdlem16  46478  fourierdlem18  46480  fourierdlem20  46482  fourierdlem21  46483  fourierdlem22  46484  fourierdlem25  46487  fourierdlem37  46499  fourierdlem42  46504  fourierdlem50  46511  fourierdlem52  46513  fourierdlem62  46523  fourierdlem64  46525  fourierdlem66  46527  fourierdlem68  46529  fourierdlem74  46535  fourierdlem75  46536  fourierdlem76  46537  fourierdlem79  46540  fourierdlem83  46544  fourierdlem95  46556  fourierdlem101  46562  fourierdlem102  46563  fourierdlem103  46564  fourierdlem104  46565  fourierdlem112  46573  fourierdlem114  46575  sqwvfoura  46583  sqwvfourb  46584  fouriersw  46586  etransclem24  46613  etransclem48  46637  sge0sn  46734  sge0tsms  46735  sge0f1o  46737  sge0pr  46749  sge0resplit  46761  sge0split  46764  sge0iunmptlemre  46770  sge0isummpt2  46787  carageniuncllem1  46876  hoicvr  46903  hoicvrrex  46911  hoidmvlelem2  46951  hspmbl  46984  smfmullem4  47149  chnsuslle  47236  lamberte  47245  rehalfge1  47692  prmdvdsfmtnof1lem1  47941  prmdvdsfmtnof  47943  upgrimpthslem2  48265  upgrimpths  48266  oddibas  48530  2zrngbas  48599  2zrng0  48601  dmtposss  49232  tposres3  49237  sepfsepc  49284  uptrlem1  49566  uptrlem2  49567  uptrlem3  49568  uptra  49571  uptrar  49572  uobeqw  49575  uptr2  49577  uptr2a  49578  fucoppcfunc  49768  aacllem  50157  amgmlemALT  50159