Theorem sstri 3948

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

Syntax hints:   ⊆ wss 3907

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

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

This theorem is referenced by:  snsstp1  4777  snsstp2  4778  uniintsn  4945  elopabran  5536  ssrnres  6167  cossxp  6262  foimacnv  6828  ssimaex  6956  riotassuni  7397  oprabss  7508  dmexg  7886  rnexg  7887  mptmpoopabbrd  8066  fparlem3  8097  fparlem4  8098  snopsuppss  8163  tposssxp  8214  naddunif  8668  naddasslem1  8669  naddasslem2  8670  mapsspw  8864  sbthlem5  9067  sbthlem7  9069  cnvimamptfin  9298  marypha1lem  9381  ordtypelem4  9471  hartogslem1  9492  ttrclco  9675  cottrcl  9676  tc2  9697  frmin  9709  frrlem16  9718  tz9.12lem1  9747  rankval4  9827  rankxpl  9835  rankmapu  9838  rankxplim  9839  djuin  9892  infxpenlem  9985  ackbij1lem18  10207  cflm  10221  fin23lem29  10313  hsmexlem4  10401  hsmexlem5  10402  brdom3  10500  brdom5  10501  brdom4  10502  smobeth  10559  pwfseqlem3  10633  wundm  10701  wunrn  10702  wunex2  10711  ltsopi  10861  dmaddpi  10863  dmmulpi  10864  nqerf  10903  ltrelxr  11258  uzssre  12872  uzwo2  12924  infssuzle  12943  infssuzcl  12944  uzwo3  12955  nn0ssq  12969  nnssq  12970  qsscn  12972  rpnnen1lem3  12991  rpnnen1lem5  12993  dflt2  13161  ioosscn  13423  unitsscn  13515  fzval2  13526  fzossz  13696  fzossnn  13728  injresinj  13808  flval3  13836  uzsup  13884  uzrdgfni  13982  expcl2lem  14097  rpexpcl  14104  expge0  14122  expge1  14123  hashxrcl  14381  seqcoll  14489  xptrrel  15005  trclublem  15020  01sqrexlem3  15283  limsupval2  15519  limsupgre  15520  rlimpm  15539  rlimclim  15585  isercolllem1  15704  isercolllem2  15705  isercoll  15707  caurcvg  15716  caucvg  15718  summolem2a  15754  summolem2  15755  zsum  15757  fsumcvg3  15768  fsumrpcl  15776  fsumge0  15835  climfsum  15860  ackbijnn  15870  prodmolem2a  15976  prodmolem2  15977  zprod  15979  fprodrpcl  15998  fprodge0  16035  fprodge1  16037  rprisefaccl  16065  divalglem8  16446  sadaddlem  16512  lcmfval  16667  isprm3  16729  maxprmfct  16756  pclem  16886  prmreclem1  16964  prmreclem2  16965  prmreclem3  16966  1arith  16975  4sqlem11  17003  ramtlecl  17048  ramcl2lem  17057  ramxrcl  17065  prmgaplem3  17101  prmgaplem4  17102  cshwshashlem1  17143  structfn  17204  strleun  17205  ressbasss  17287  ressbasss2  17289  srngbase  17351  srngplusg  17352  srngmulr  17353  lmodbase  17367  lmodplusg  17368  lmodsca  17369  ipsbase  17378  ipsaddg  17379  ipsmulr  17380  ipssca  17381  ipsvsca  17382  ipsip  17383  phlbase  17388  phlplusg  17389  phlsca  17390  phlvsca  17391  phlip  17392  odrngbas  17445  odrngplusg  17446  odrngmulr  17447  odrngtset  17448  odrngle  17449  odrngds  17450  prdsvallem  17495  prdsval  17496  prdssca  17497  prdsbas  17498  prdsplusg  17499  prdsmulr  17500  prdsvsca  17501  prdsip  17502  prdsle  17503  prdsds  17505  prdstset  17507  prdshom  17508  prdsco  17509  imasbas  17554  imasds  17555  imasplusg  17559  imasmulr  17560  imassca  17561  imasvsca  17562  imasip  17563  imastset  17564  imasle  17565  wunfunc  17946  fullfunc  17953  fthfunc  17954  isfull  17957  isfth  17961  wunnat  18004  dmcoass  18111  catcisolem  18155  catciso  18156  catcoppccl  18162  catcfuccl  18163  catcxpccl  18251  ipobas  18575  ipolerval  18576  ipotset  18577  psdmrn  18617  psss  18624  ledm  18634  lern  18635  dirdm  18644  dirge  18647  mulgfval  19123  mvdco  19503  f1omvdconj  19504  gexex  19911  gsumval3  19965  lssacs  21054  cnfldbas  21483  mpocnfldadd  21484  mpocnfldmul  21486  cnfldcj  21488  cnfldtset  21489  cnfldle  21490  cnfldds  21491  cnfldunif  21492  rge0srg  21545  zntoslem  21663  asplss  21980  aspsubrg  21982  psrass1lem  22040  psrbas  22041  psrplusg  22044  psrmulr  22049  psrsca  22054  psrvscafval  22055  psrass1  22070  psrass23l  22073  psrcom  22074  psrass23  22075  psropprmul  22354  coe1mul2  22387  ofco2  22565  toponsspwpw  23036  dmtopon  23037  leordtval2  23326  lmbrf  23374  lmres  23414  fiuncmp  23518  comppfsc  23646  1stckgenlem  23667  kgencn3  23672  ptbasfi  23695  xkoopn  23703  txcnmpt  23738  txkgen  23766  opnfbas  23956  fmfnfmlem4  24071  tsmsxplem1  24267  trust  24343  restutop  24351  nmoffn  24825  nmofval  24828  nmogelb  24830  nmolb  24831  nmof  24833  qtopbas  24873  tgqioo  24914  re2ndc  24915  iitopon  24995  dfii3  24999  cnheiborlem  25070  bndth  25074  lebnumii  25082  pcoass  25140  cphsqrtcl  25300  lmmbrf  25378  iscauf  25396  caucfil  25399  lmclimf  25420  rrxmval  25521  rrxmet  25524  ovolfioo  25583  ovolficc  25584  ovolficcss  25585  ovolfsf  25587  ovollb  25595  ovolicc2lem3  25635  ovolicc2lem4  25636  ovolicc2  25638  volf  25645  volsup  25672  ovolfs2  25687  uniiccdif  25694  uniioovol  25695  uniiccvol  25696  uniioombllem2  25699  uniioombllem3a  25700  uniioombllem3  25701  uniioombllem4  25702  uniioombllem5  25703  uniioombl  25705  dyadmbllem  25715  dyadmbl  25716  opnmbllem  25717  opnmblALT  25719  volsup2  25721  vitalilem4  25727  vitalilem5  25728  vitali  25729  mbfimaopnlem  25771  mbflimsup  25782  i1f0  25803  i1f1  25806  itg11  25807  itg2mulc  25863  itg2gt0  25876  ellimc2  25993  limcresi  26001  dvreslem  26025  dvres2lem  26026  dvaddbr  26054  dvmulbr  26055  dvlipcn  26110  c1liplem1  26112  lhop1lem  26129  lhop1  26130  lhop2  26131  lhop  26132  dvfsumrlim  26147  ftc1cn  26159  itgsubstlem  26164  itgsubst  26165  itgpowd  26166  mdegleb  26178  mdeglt  26179  mdegldg  26180  mdegxrcl  26181  mdegcl  26183  mdegaddle  26188  mdegmullem  26192  deg1mul3le  26231  ig1peu  26289  ig1pdvds  26294  aacjcl  26445  aannenlem2  26447  aannenlem3  26448  aalioulem2  26451  taylfval  26476  radcnvcl  26534  radcnvlt1  26535  radcnvle  26537  abelth  26558  abelth2  26559  pilem2  26569  pilem3  26570  pige3ALT  26639  recosf1o  26654  resinf1o  26655  tanord1  26656  logcn  26766  dvlog  26770  dvlog2lem  26771  efopn  26777  logtayl  26779  cxpcn3  26867  loglesqrt  26880  ssscongptld  26941  leibpi  27061  efrlim  27088  jensenlem1  27105  jensenlem2  27106  jensen  27107  amgm  27109  lgamgulmlem2  27148  ftalem5  27195  efnnfsumcl  27221  efchtdvds  27277  mpodvdsmulf1o  27312  fsumdvdsmul  27313  dvdsmulf1o  27314  lgsfcl2  27421  2sqlem6  27541  2sqlem8  27544  2sqlem9  27545  rpvmasumlem  27605  rpvmasum2  27630  dchrisum0re  27631  dchrisum0lem3  27637  dchrisum0  27638  rplogsum  27645  dirith2  27646  noextendseq  27785  oldf  27984  leftssno  28020  rightssno  28021  addbdaylem  28164  mulsproplem12  28274  mulsproplem13  28275  mulsproplem14  28276  mulsasslem3  28312  precsexlem11  28364  oncutlt  28411  bdayons  28423  nnssno  28469  axtgcgrrflx  28685  axtgcgrid  28686  axtgsegcon  28687  axtg5seg  28688  axtgbtwnid  28689  axtgpasch  28690  axtgcont1  28691  tgcgr4  28754  motcgrg  28767  tglng  28769  upgrss  29343  pthdivtx  29981  disjxwwlkn  30167  ex-fpar  30718  nmlno0lem  31050  hlimcaui  31493  chsspwh  31504  shsss  31570  chintcli  31588  shsleji  31627  shub1i  31631  shsval2i  31644  lejdii  31795  spanuni  31801  sshhococi  31803  spansnpji  31835  osumcori  31900  5oai  31918  3oalem6  31924  3oai  31925  pjssmii  31938  mayete3i  31985  mayetes3i  31986  nmlnop0iALT  32252  imaelshi  32315  pjnmopi  32405  pjclem1  32452  pjci  32457  mdslmd1lem1  32582  shatomistici  32618  hatomistici  32619  chpssati  32620  xppreima  32898  iundisjfi  33049  iundisj2fi  33050  fprodex01  33077  indsumin  33089  xrsmulgzz  33237  fsumrp0cl  33249  gsummpt2co  33276  cycpmfv2  33342  cycpmrn  33371  rlocbas  33496  rlocaddval  33497  rlocmulval  33498  1fldgenq  33553  xrge0slmod  33578  lsmsnorb  33615  idlsrgbas  33706  idlsrgplusg  33707  idlsrgmulr  33709  idlsrgtset  33710  selvply1rhmlemb  33821  esplyind  33877  vietalem  33881  constrextdg2  34051  ordtconnlem1  34226  xrge0iifhom  34239  lmlimxrge0  34250  lmxrge0  34254  esumcst  34365  esumpfinvallem  34376  esumpfinval  34377  esumpfinvalf  34378  esumcvg  34388  imambfm  34564  elmbfmvol2  34569  sxbrsigalem3  34574  sxbrsigalem2  34588  sxbrsigalem4  34589  sitgclg  34644  eulerpartlem1  34669  eulerpartlemgvv  34678  eulerpartlemgh  34680  eulerpartlemgf  34681  ballotlemfc0  34795  ballotlemfcc  34796  ballotlemiex  34804  ballotlemsup  34807  ballotlemsima  34818  ballotlemrv2  34824  ballotth  34840  signsplypnf  34849  signsply0  34850  rpsqrtcn  34892  itgexpif  34905  fsum2dsub  34906  reprfi2  34922  chtvalz  34928  breprexplemc  34931  breprexpnat  34933  circlemeth  34939  circlemethnat  34940  circlevma  34941  circlemethhgt  34942  hgt750lemd  34947  hgt750lema  34956  tgoldbachgtde  34959  tgoldbachgtda  34960  tgoldbachgt  34962  bnj1145  35293  bnj1286  35319  subfacp1lem2a  35538  erdszelem4  35552  erdszelem5  35553  erdszelem7  35555  erdszelem8  35556  kur14lem7  35570  kur14lem9  35572  resconn  35604  iccllysconn  35608  txpss3v  36234  txprel  36235  limitssson  36267  finminlem  36686  tailf  36743  filnetlem3  36748  onint1  36817  ttcuniun  36878  bj-unrab  37418  bj-2upln1upl  37516  bj-imdirco  37689  bj-rvecssabl  37805  taupilem2  37821  taupi  37822  poimirlem3  38129  poimirlem30  38156  poimirlem31  38157  poimirlem32  38158  broucube  38160  opnmbllem0  38162  mblfinlem1  38163  mblfinlem2  38164  mblfinlem3  38165  mblfinlem4  38166  ismblfin  38167  mbfposadd  38173  cnambfre  38174  itg2addnc  38180  ftc1cnnclem  38197  ftc1cnnc  38198  ftc1anclem3  38201  ftc1anclem7  38205  ftc1anc  38207  ftc2nc  38208  dvreasin  38212  dvreacos  38213  areacirclem1  38214  areacirclem2  38215  areacirc  38219  caures  38266  reheibor  38345  xrnss3v  38887  xrnrel  38888  atlatmstc  39950  atlatle  39951  pmaple  40392  sspadd1  40446  sspadd2  40447  dvrelog2  42688  dvrelog3  42689  rpsscn  42915  sumcubes  42929  redvmptabs  42976  diophin  43360  4rexfrabdioph  43382  6rexfrabdioph  43383  irrapxlem1  43406  irrapx1  43412  rmxyelqirr  43494  monotuz  43525  jm2.27dlem5  43597  hbtlem2  43708  algbase  43758  algaddg  43759  algmulr  43760  algsca  43761  algvsca  43762  arearect  43799  areaquad  43800  rtrclex  44200  trclubgNEW  44201  trclexi  44203  rtrclexi  44204  cnvtrcl0  44209  dfrtrcl5  44212  trrelsuperrel2dg  44254  relexpaddss  44301  brtrclfv2  44310  frege131d  44347  xphe  44364  clsk3nimkb  44623  gneispace  44717  k0004val0  44737  inaex  44866  lhe4.4ex1a  44898  uzmptshftfval  44915  binomcxplemdvbinom  44922  binomcxplemcvg  44923  binomcxplemnotnn0  44925  relopabVD  45468  dmwf  45533  rnwf  45534  fzisoeu  45878  fzsscn  45889  fzssre  45892  fzossuz  45955  zssxr  45971  uzssre2  45980  supminfxr  46037  uzsscn  46048  rpssxr  46053  uzinico  46134  limcresiooub  46215  limcresioolb  46216  limcleqr  46217  limclner  46224  limclr  46228  limsupequzmpt2  46291  liminfval2  46341  liminfequzmpt2  46364  icccncfext  46460  cncficcgt0  46461  ioodvbdlimc1lem2  46505  ioodvbdlimc2lem  46507  dvnprodlem2  46520  itgsin0pilem1  46523  itgsinexplem1  46527  itgsinexp  46528  dirkercncflem2  46677  fourierdlem16  46696  fourierdlem18  46698  fourierdlem20  46700  fourierdlem21  46701  fourierdlem22  46702  fourierdlem25  46705  fourierdlem37  46717  fourierdlem42  46722  fourierdlem50  46729  fourierdlem52  46731  fourierdlem62  46741  fourierdlem64  46743  fourierdlem66  46745  fourierdlem68  46747  fourierdlem74  46753  fourierdlem75  46754  fourierdlem76  46755  fourierdlem79  46758  fourierdlem83  46762  fourierdlem95  46774  fourierdlem101  46780  fourierdlem102  46781  fourierdlem103  46782  fourierdlem104  46783  fourierdlem112  46791  fourierdlem114  46793  sqwvfoura  46801  sqwvfourb  46802  fouriersw  46804  etransclem24  46831  etransclem48  46855  sge0sn  46952  sge0tsms  46953  sge0f1o  46955  sge0pr  46967  sge0resplit  46979  sge0split  46982  sge0iunmptlemre  46988  sge0isummpt2  47005  carageniuncllem1  47094  hoicvr  47121  hoicvrrex  47129  hoidmvlelem2  47169  hspmbl  47202  smfmullem4  47367  chnsuslle  47456  lamberte  47481  rehalfge1  47932  prmdvdsfmtnof1lem1  48192  prmdvdsfmtnof  48194  upgrimpthslem2  48529  upgrimpths  48530  oddibas  48794  2zrngbas  48863  2zrng0  48865  dmtposss  49506  tposres3  49511  sepfsepc  49558  uptrlem1  49840  uptrlem2  49841  uptrlem3  49842  uptra  49845  uptrar  49846  uobeqw  49849  uptr2  49851  uptr2a  49852  fucoppcfunc  50042  aacllem  50431  amgmlemALT  50433