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

Syntax hints:   ⊆ wss 3889

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 3906

This theorem is referenced by:  snsstp1  4759  snsstp2  4760  uniintsn  4927  elopabran  5516  ssrnres  6142  cossxp  6236  foimacnv  6797  ssimaex  6925  riotassuni  7364  oprabss  7475  dmexg  7852  rnexg  7853  fabexgOLD  7890  mptmpoopabbrd  8033  fparlem3  8064  fparlem4  8065  snopsuppss  8129  tposssxp  8180  naddunif  8629  naddasslem1  8630  naddasslem2  8631  mapsspw  8826  sbthlem5  9029  sbthlem7  9031  cnvimamptfin  9263  marypha1lem  9346  ordtypelem4  9436  hartogslem1  9457  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  11206  uzssre  12810  uzwo2  12862  infssuzle  12881  infssuzcl  12882  uzwo3  12893  nn0ssq  12907  nnssq  12908  qsscn  12910  rpnnen1lem3  12929  rpnnen1lem5  12931  dflt2  13099  ioosscn  13361  unitsscn  13453  fzval2  13464  fzossz  13634  fzossnn  13666  injresinj  13746  flval3  13774  uzsup  13822  uzrdgfni  13920  expcl2lem  14035  rpexpcl  14042  expge0  14060  expge1  14061  hashxrcl  14319  seqcoll  14426  xptrrel  14942  trclublem  14957  01sqrexlem3  15206  limsupval2  15442  limsupgre  15443  rlimpm  15462  rlimclim  15508  isercolllem1  15627  isercolllem2  15628  isercoll  15630  caurcvg  15639  caucvg  15641  summolem2a  15677  summolem2  15678  zsum  15680  fsumcvg3  15691  fsumrpcl  15699  fsumge0  15758  climfsum  15783  ackbijnn  15793  prodmolem2a  15899  prodmolem2  15900  zprod  15902  fprodrpcl  15921  fprodge0  15958  fprodge1  15960  rprisefaccl  15988  divalglem8  16369  sadaddlem  16435  lcmfval  16590  isprm3  16652  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  17476  imasds  17477  imasplusg  17481  imasmulr  17482  imassca  17483  imasvsca  17484  imasip  17485  imastset  17486  imasle  17487  wunfunc  17868  fullfunc  17875  fthfunc  17876  isfull  17879  isfth  17883  wunnat  17926  dmcoass  18033  catcisolem  18077  catciso  18078  catcoppccl  18084  catcfuccl  18085  catcxpccl  18173  ipobas  18497  ipolerval  18498  ipotset  18499  psdmrn  18539  psss  18546  ledm  18556  lern  18557  dirdm  18566  dirge  18569  mulgfval  19045  mvdco  19420  f1omvdconj  19421  gexex  19828  gsumval3  19882  lssacs  20962  cnfldbas  21356  mpocnfldadd  21357  mpocnfldmul  21359  cnfldcj  21361  cnfldtset  21362  cnfldle  21363  cnfldds  21364  cnfldunif  21365  rge0srg  21418  zntoslem  21536  asplss  21853  aspsubrg  21855  psrass1lem  21912  psrbas  21913  psrplusg  21916  psrmulr  21921  psrsca  21926  psrvscafval  21927  psrass1  21942  psrass23l  21945  psrcom  21946  psrass23  21947  psropprmul  22201  coe1mul2  22234  ofco2  22416  toponsspwpw  22887  dmtopon  22888  leordtval2  23177  lmbrf  23225  lmres  23265  fiuncmp  23369  comppfsc  23497  1stckgenlem  23518  kgencn3  23523  ptbasfi  23546  xkoopn  23554  txcnmpt  23589  txkgen  23617  opnfbas  23807  fmfnfmlem4  23922  tsmsxplem1  24118  trust  24194  restutop  24202  nmoffn  24676  nmofval  24679  nmogelb  24681  nmolb  24682  nmof  24684  qtopbas  24724  tgqioo  24765  re2ndc  24766  iitopon  24846  dfii3  24850  cnheiborlem  24921  bndth  24925  lebnumii  24933  pcoass  24991  cphsqrtcl  25151  lmmbrf  25229  iscauf  25247  caucfil  25250  lmclimf  25271  rrxmval  25372  rrxmet  25375  ovolfioo  25434  ovolficc  25435  ovolficcss  25436  ovolfsf  25438  ovollb  25446  ovolicc2lem3  25486  ovolicc2lem4  25487  ovolicc2  25489  volf  25496  volsup  25523  ovolfs2  25538  uniiccdif  25545  uniioovol  25546  uniiccvol  25547  uniioombllem2  25550  uniioombllem3a  25551  uniioombllem3  25552  uniioombllem4  25553  uniioombllem5  25554  uniioombl  25556  dyadmbllem  25566  dyadmbl  25567  opnmbllem  25568  opnmblALT  25570  volsup2  25572  vitalilem4  25578  vitalilem5  25579  vitali  25580  mbfimaopnlem  25622  mbflimsup  25633  i1f0  25654  i1f1  25657  itg11  25658  itg2mulc  25714  itg2gt0  25727  ellimc2  25844  limcresi  25852  dvreslem  25876  dvres2lem  25877  dvaddbr  25905  dvmulbr  25906  dvlipcn  25961  c1liplem1  25963  lhop1lem  25980  lhop1  25981  lhop2  25982  lhop  25983  dvfsumrlim  25998  ftc1cn  26010  itgsubstlem  26015  itgsubst  26016  itgpowd  26017  mdegleb  26029  mdeglt  26030  mdegldg  26031  mdegxrcl  26032  mdegcl  26034  mdegaddle  26039  mdegmullem  26043  deg1mul3le  26082  ig1peu  26140  ig1pdvds  26145  aacjcl  26293  aannenlem2  26295  aannenlem3  26296  aalioulem2  26299  taylfval  26324  radcnvcl  26382  radcnvlt1  26383  radcnvle  26385  abelth  26406  abelth2  26407  pilem2  26417  pilem3  26418  pige3ALT  26484  recosf1o  26499  resinf1o  26500  tanord1  26501  logcn  26611  dvlog  26615  dvlog2lem  26616  efopn  26622  logtayl  26624  cxpcn3  26712  loglesqrt  26725  ssscongptld  26786  leibpi  26906  efrlim  26933  jensenlem1  26950  jensenlem2  26951  jensen  26952  amgm  26954  lgamgulmlem2  26993  ftalem5  27040  efnnfsumcl  27066  efchtdvds  27122  mpodvdsmulf1o  27157  fsumdvdsmul  27158  dvdsmulf1o  27159  lgsfcl2  27266  2sqlem6  27386  2sqlem8  27389  2sqlem9  27390  rpvmasumlem  27450  rpvmasum2  27475  dchrisum0re  27476  dchrisum0lem3  27482  dchrisum0  27483  rplogsum  27490  dirith2  27491  noextendseq  27631  oldf  27829  leftssno  27865  rightssno  27866  addbdaylem  28009  mulsproplem12  28119  mulsproplem13  28120  mulsproplem14  28121  mulsasslem3  28157  precsexlem11  28209  oncutlt  28256  bdayons  28268  nnssno  28314  axtgcgrrflx  28530  axtgcgrid  28531  axtgsegcon  28532  axtg5seg  28533  axtgbtwnid  28534  axtgpasch  28535  axtgcont1  28536  tgcgr4  28599  motcgrg  28612  tglng  28614  upgrss  29157  pthdivtx  29795  disjxwwlkn  29981  ex-fpar  30532  nmlno0lem  30864  hlimcaui  31307  chsspwh  31318  shsss  31384  chintcli  31402  shsleji  31441  shub1i  31445  shsval2i  31458  lejdii  31609  spanuni  31615  sshhococi  31617  spansnpji  31649  osumcori  31714  5oai  31732  3oalem6  31738  3oai  31739  pjssmii  31752  mayete3i  31799  mayetes3i  31800  nmlnop0iALT  32066  imaelshi  32129  pjnmopi  32219  pjclem1  32266  pjci  32271  mdslmd1lem1  32396  shatomistici  32432  hatomistici  32433  chpssati  32434  xppreima  32718  iundisjfi  32869  iundisj2fi  32870  fprodex01  32898  indsumin  32921  xrsmulgzz  33069  fsumrp0cl  33081  gsummpt2co  33109  cycpmfv2  33175  cycpmrn  33204  rlocbas  33328  rlocaddval  33329  rlocmulval  33330  1fldgenq  33383  xrge0slmod  33408  lsmsnorb  33451  idlsrgbas  33564  idlsrgplusg  33565  idlsrgmulr  33567  idlsrgtset  33568  esplyind  33719  vietalem  33723  constrextdg2  33893  ordtconnlem1  34068  xrge0iifhom  34081  lmlimxrge0  34092  lmxrge0  34096  esumcst  34207  esumpfinvallem  34218  esumpfinval  34219  esumpfinvalf  34220  esumcvg  34230  imambfm  34406  elmbfmvol2  34411  sxbrsigalem3  34416  sxbrsigalem2  34430  sxbrsigalem4  34431  sitgclg  34486  eulerpartlem1  34511  eulerpartlemgvv  34520  eulerpartlemgh  34522  eulerpartlemgf  34523  ballotlemfc0  34637  ballotlemfcc  34638  ballotlemiex  34646  ballotlemsup  34649  ballotlemsima  34660  ballotlemrv2  34666  ballotth  34682  signsplypnf  34694  signsply0  34695  rpsqrtcn  34737  itgexpif  34750  fsum2dsub  34751  reprfi2  34767  chtvalz  34773  breprexplemc  34776  breprexpnat  34778  circlemeth  34784  circlemethnat  34785  circlevma  34786  circlemethhgt  34787  hgt750lemd  34792  hgt750lema  34801  tgoldbachgtde  34804  tgoldbachgtda  34805  tgoldbachgt  34807  bnj1145  35135  bnj1286  35161  subfacp1lem2a  35362  erdszelem4  35376  erdszelem5  35377  erdszelem7  35379  erdszelem8  35380  kur14lem7  35394  kur14lem9  35396  resconn  35428  iccllysconn  35432  txpss3v  36058  txprel  36059  limitssson  36091  finminlem  36500  tailf  36557  filnetlem3  36562  onint1  36631  ttcuniun  36692  bj-unrab  37233  bj-2upln1upl  37331  bj-imdirco  37504  bj-rvecssabl  37620  taupilem2  37636  taupi  37637  poimirlem3  37944  poimirlem30  37971  poimirlem31  37972  poimirlem32  37973  broucube  37975  opnmbllem0  37977  mblfinlem1  37978  mblfinlem2  37979  mblfinlem3  37980  mblfinlem4  37981  ismblfin  37982  mbfposadd  37988  cnambfre  37989  itg2addnc  37995  ftc1cnnclem  38012  ftc1cnnc  38013  ftc1anclem3  38016  ftc1anclem7  38020  ftc1anc  38022  ftc2nc  38023  dvreasin  38027  dvreacos  38028  areacirclem1  38029  areacirclem2  38030  areacirc  38034  caures  38081  reheibor  38160  xrnss3v  38702  xrnrel  38703  atlatmstc  39765  atlatle  39766  pmaple  40207  sspadd1  40261  sspadd2  40262  dvrelog2  42503  dvrelog3  42504  rpsscn  42731  sumcubes  42745  redvmptabs  42792  diophin  43204  4rexfrabdioph  43226  6rexfrabdioph  43227  irrapxlem1  43250  irrapx1  43256  rmxyelqirr  43338  monotuz  43369  jm2.27dlem5  43441  hbtlem2  43552  algbase  43602  algaddg  43603  algmulr  43604  algsca  43605  algvsca  43606  arearect  43643  areaquad  43644  rtrclex  44044  trclubgNEW  44045  trclexi  44047  rtrclexi  44048  cnvtrcl0  44053  dfrtrcl5  44056  trrelsuperrel2dg  44098  relexpaddss  44145  brtrclfv2  44154  frege131d  44191  xphe  44208  clsk3nimkb  44467  gneispace  44561  k0004val0  44581  inaex  44724  lhe4.4ex1a  44756  uzmptshftfval  44773  binomcxplemdvbinom  44780  binomcxplemcvg  44781  binomcxplemnotnn0  44783  relopabVD  45327  dmwf  45392  rnwf  45393  fzisoeu  45733  fzsscn  45744  fzssre  45747  fzossuz  45810  zssxr  45826  uzssre2  45835  supminfxr  45892  uzsscn  45903  rpssxr  45908  uzinico  45989  limcresiooub  46070  limcresioolb  46071  limcleqr  46072  limclner  46079  limclr  46083  limsupequzmpt2  46146  liminfval2  46196  liminfequzmpt2  46219  icccncfext  46315  cncficcgt0  46316  ioodvbdlimc1lem2  46360  ioodvbdlimc2lem  46362  dvnprodlem2  46375  itgsin0pilem1  46378  itgsinexplem1  46382  itgsinexp  46383  dirkercncflem2  46532  fourierdlem16  46551  fourierdlem18  46553  fourierdlem20  46555  fourierdlem21  46556  fourierdlem22  46557  fourierdlem25  46560  fourierdlem37  46572  fourierdlem42  46577  fourierdlem50  46584  fourierdlem52  46586  fourierdlem62  46596  fourierdlem64  46598  fourierdlem66  46600  fourierdlem68  46602  fourierdlem74  46608  fourierdlem75  46609  fourierdlem76  46610  fourierdlem79  46613  fourierdlem83  46617  fourierdlem95  46629  fourierdlem101  46635  fourierdlem102  46636  fourierdlem103  46637  fourierdlem104  46638  fourierdlem112  46646  fourierdlem114  46648  sqwvfoura  46656  sqwvfourb  46657  fouriersw  46659  etransclem24  46686  etransclem48  46710  sge0sn  46807  sge0tsms  46808  sge0f1o  46810  sge0pr  46822  sge0resplit  46834  sge0split  46837  sge0iunmptlemre  46843  sge0isummpt2  46860  carageniuncllem1  46949  hoicvr  46976  hoicvrrex  46984  hoidmvlelem2  47024  hspmbl  47057  smfmullem4  47222  chnsuslle  47311  lamberte  47336  rehalfge1  47787  prmdvdsfmtnof1lem1  48047  prmdvdsfmtnof  48049  upgrimpthslem2  48384  upgrimpths  48385  oddibas  48649  2zrngbas  48718  2zrng0  48720  dmtposss  49351  tposres3  49356  sepfsepc  49403  uptrlem1  49685  uptrlem2  49686  uptrlem3  49687  uptra  49690  uptrar  49691  uobeqw  49694  uptr2  49696  uptr2a  49697  fucoppcfunc  49887  aacllem  50276  amgmlemALT  50278