Theorem sstri 3968

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

Syntax hints:   ⊆ wss 3926

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 3943

This theorem is referenced by:  snsstp1  4792  snsstp2  4793  uniintsn  4961  elopabran  5537  ssrnres  6167  cossxp  6261  foimacnv  6834  ssimaex  6963  riotassuni  7400  oprabss  7513  dmexg  7895  rnexg  7896  fabexgOLD  7933  mptmpoopabbrd  8077  fparlem3  8111  fparlem4  8112  snopsuppss  8176  tposssxp  8227  naddunif  8703  naddasslem1  8704  naddasslem2  8705  mapsspw  8890  sbthlem5  9099  sbthlem7  9101  cnvimamptfin  9363  marypha1lem  9443  ordtypelem4  9533  hartogslem1  9554  ttrclco  9730  cottrcl  9731  tc2  9754  frmin  9761  frrlem16  9770  tz9.12lem1  9799  rankval4  9879  rankxpl  9887  rankmapu  9890  rankxplim  9891  djuin  9930  infxpenlem  10025  ackbij1lem18  10248  cflm  10262  fin23lem29  10353  hsmexlem4  10441  hsmexlem5  10442  brdom3  10540  brdom5  10541  brdom4  10542  smobeth  10598  pwfseqlem3  10672  wundm  10740  wunrn  10741  wunex2  10750  ltsopi  10900  dmaddpi  10902  dmmulpi  10903  nqerf  10942  ltrelxr  11294  uzssre  12872  uzwo2  12926  infssuzle  12945  infssuzcl  12946  uzwo3  12957  nn0ssq  12971  nnssq  12972  qsscn  12974  rpnnen1lem3  12993  rpnnen1lem5  12995  dflt2  13162  ioosscn  13423  unitsscn  13515  fzval2  13525  fzossz  13694  fzossnn  13726  injresinj  13802  flval3  13830  uzsup  13878  uzrdgfni  13974  expcl2lem  14089  rpexpcl  14096  expge0  14114  expge1  14115  hashxrcl  14373  seqcoll  14480  xptrrel  14997  trclublem  15012  01sqrexlem3  15261  limsupval2  15494  limsupgre  15495  rlimpm  15514  rlimclim  15560  isercolllem1  15679  isercolllem2  15680  isercoll  15682  caurcvg  15691  caucvg  15693  summolem2a  15729  summolem2  15730  zsum  15732  fsumcvg3  15743  fsumrpcl  15751  fsumge0  15809  climfsum  15834  ackbijnn  15842  prodmolem2a  15948  prodmolem2  15949  zprod  15951  fprodrpcl  15970  fprodge0  16007  fprodge1  16009  rprisefaccl  16037  divalglem8  16417  sadaddlem  16483  lcmfval  16638  isprm3  16700  maxprmfct  16726  pclem  16856  prmreclem1  16934  prmreclem2  16935  prmreclem3  16936  1arith  16945  4sqlem11  16973  ramtlecl  17018  ramcl2lem  17027  ramxrcl  17035  prmgaplem3  17071  prmgaplem4  17072  cshwshashlem1  17113  structfn  17173  strleun  17174  ressbasss  17258  ressbasss2  17260  srngbase  17322  srngplusg  17323  srngmulr  17324  lmodbase  17338  lmodplusg  17339  lmodsca  17340  ipsbase  17349  ipsaddg  17350  ipsmulr  17351  ipssca  17352  ipsvsca  17353  ipsip  17354  phlbase  17359  phlplusg  17360  phlsca  17361  phlvsca  17362  phlip  17363  odrngbas  17416  odrngplusg  17417  odrngmulr  17418  odrngtset  17419  odrngle  17420  odrngds  17421  prdsvallem  17466  prdsval  17467  prdssca  17468  prdsbas  17469  prdsplusg  17470  prdsmulr  17471  prdsvsca  17472  prdsip  17473  prdsle  17474  prdsds  17476  prdstset  17478  prdshom  17479  prdsco  17480  imasbas  17524  imasds  17525  imasplusg  17529  imasmulr  17530  imassca  17531  imasvsca  17532  imasip  17533  imastset  17534  imasle  17535  wunfunc  17912  fullfunc  17919  fthfunc  17920  isfull  17923  isfth  17927  wunnat  17970  dmcoass  18077  catcisolem  18121  catciso  18122  catcoppccl  18128  catcfuccl  18129  catcxpccl  18217  ipobas  18539  ipolerval  18540  ipotset  18541  psdmrn  18581  psss  18588  ledm  18598  lern  18599  dirdm  18608  dirge  18611  mulgfval  19050  mvdco  19424  f1omvdconj  19425  gexex  19832  gsumval3  19886  lssacs  20922  cnfldbas  21317  mpocnfldadd  21318  mpocnfldmul  21320  cnfldcj  21322  cnfldtset  21323  cnfldle  21324  cnfldds  21325  cnfldunif  21326  cnfldbasOLD  21332  cnfldaddOLD  21333  cnfldmulOLD  21334  cnfldcjOLD  21335  cnfldtsetOLD  21336  cnfldleOLD  21337  cnflddsOLD  21338  cnfldunifOLD  21339  rge0srg  21404  zntoslem  21515  asplss  21832  aspsubrg  21834  psrass1lem  21890  psrbas  21891  psrplusg  21894  psrmulr  21900  psrsca  21905  psrvscafval  21906  psrass1  21922  psrass23l  21925  psrcom  21926  psrass23  21927  psropprmul  22171  coe1mul2  22204  ofco2  22387  toponsspwpw  22858  dmtopon  22859  leordtval2  23148  lmbrf  23196  lmres  23236  fiuncmp  23340  comppfsc  23468  1stckgenlem  23489  kgencn3  23494  ptbasfi  23517  xkoopn  23525  txcnmpt  23560  txkgen  23588  opnfbas  23778  fmfnfmlem4  23893  tsmsxplem1  24089  trust  24166  restutop  24174  nmoffn  24648  nmofval  24651  nmogelb  24653  nmolb  24654  nmof  24656  qtopbas  24696  tgqioo  24737  re2ndc  24738  iitopon  24821  dfii3  24825  iimulcnOLD  24884  cnheiborlem  24902  bndth  24906  lebnumii  24914  reparphtiOLD  24946  pcoass  24973  cphsqrtcl  25134  lmmbrf  25212  iscauf  25230  caucfil  25233  lmclimf  25254  rrxmval  25355  rrxmet  25358  ovolfioo  25418  ovolficc  25419  ovolficcss  25420  ovolfsf  25422  ovollb  25430  ovolicc2lem3  25470  ovolicc2lem4  25471  ovolicc2  25473  volf  25480  volsup  25507  ovolfs2  25522  uniiccdif  25529  uniioovol  25530  uniiccvol  25531  uniioombllem2  25534  uniioombllem3a  25535  uniioombllem3  25536  uniioombllem4  25537  uniioombllem5  25538  uniioombl  25540  dyadmbllem  25550  dyadmbl  25551  opnmbllem  25552  opnmblALT  25554  volsup2  25556  vitalilem4  25562  vitalilem5  25563  vitali  25564  mbfimaopnlem  25606  mbflimsup  25617  i1f0  25638  i1f1  25641  itg11  25642  itg2mulc  25698  itg2gt0  25711  ellimc2  25828  limcresi  25836  dvreslem  25860  dvres2lem  25861  dvaddbr  25890  dvmulbr  25891  dvmulbrOLD  25892  dvlipcn  25949  c1liplem1  25951  lhop1lem  25968  lhop1  25969  lhop2  25970  lhop  25971  dvfsumrlim  25988  ftc1cn  26000  itgsubstlem  26005  itgsubst  26006  itgpowd  26007  mdegleb  26019  mdeglt  26020  mdegldg  26021  mdegxrcl  26022  mdegcl  26024  mdegaddle  26029  mdegmullem  26033  deg1mul3le  26072  ig1peu  26130  ig1pdvds  26135  aacjcl  26285  aannenlem2  26287  aannenlem3  26288  aalioulem2  26291  taylfval  26316  radcnvcl  26376  radcnvlt1  26377  radcnvle  26379  abelth  26401  abelth2  26402  pilem2  26412  pilem3  26413  pige3ALT  26479  recosf1o  26494  resinf1o  26495  tanord1  26496  logcn  26606  dvlog  26610  dvlog2lem  26611  efopn  26617  logtayl  26619  cxpcn3  26708  loglesqrt  26721  ssscongptld  26782  leibpi  26902  efrlim  26929  efrlimOLD  26930  jensenlem1  26947  jensenlem2  26948  jensen  26949  amgm  26951  lgamgulmlem2  26990  ftalem5  27037  efnnfsumcl  27063  efchtdvds  27119  mpodvdsmulf1o  27154  fsumdvdsmul  27155  dvdsmulf1o  27156  fsumdvdsmulOLD  27157  lgsfcl2  27264  2sqlem6  27384  2sqlem8  27387  2sqlem9  27388  rpvmasumlem  27448  rpvmasum2  27473  dchrisum0re  27474  dchrisum0lem3  27480  dchrisum0  27481  rplogsum  27488  dirith2  27489  noextendseq  27629  oldf  27813  leftssno  27836  rightssno  27837  addsbdaylem  27966  mulsproplem12  28070  mulsproplem13  28071  mulsproplem14  28072  mulsasslem3  28108  precsexlem11  28158  nnssno  28244  axtgcgrrflx  28387  axtgcgrid  28388  axtgsegcon  28389  axtg5seg  28390  axtgbtwnid  28391  axtgpasch  28392  axtgcont1  28393  tgcgr4  28456  motcgrg  28469  tglng  28471  upgrss  29013  pthdivtx  29655  disjxwwlkn  29841  ex-fpar  30389  nmlno0lem  30720  hlimcaui  31163  chsspwh  31174  shsss  31240  chintcli  31258  shsleji  31297  shub1i  31301  shsval2i  31314  lejdii  31465  spanuni  31471  sshhococi  31473  spansnpji  31505  osumcori  31570  5oai  31588  3oalem6  31594  3oai  31595  pjssmii  31608  mayete3i  31655  mayetes3i  31656  nmlnop0iALT  31922  imaelshi  31985  pjnmopi  32075  pjclem1  32122  pjci  32127  mdslmd1lem1  32252  shatomistici  32288  hatomistici  32289  chpssati  32290  xppreima  32569  iundisjfi  32719  iundisj2fi  32720  fprodex01  32750  indsumin  32785  xrsmulgzz  32947  fsumrp0cl  32962  gsummpt2co  32988  cycpmfv2  33071  cycpmrn  33100  rlocbas  33208  rlocaddval  33209  rlocmulval  33210  1fldgenq  33262  xrge0slmod  33309  lsmsnorb  33352  idlsrgbas  33465  idlsrgplusg  33466  idlsrgmulr  33468  idlsrgtset  33469  constrextdg2  33729  ordtconnlem1  33901  xrge0iifhom  33914  lmlimxrge0  33925  lmxrge0  33929  esumcst  34040  esumpfinvallem  34051  esumpfinval  34052  esumpfinvalf  34053  esumcvg  34063  imambfm  34240  elmbfmvol2  34245  sxbrsigalem3  34250  sxbrsigalem2  34264  sxbrsigalem4  34265  sitgclg  34320  eulerpartlem1  34345  eulerpartlemgvv  34354  eulerpartlemgh  34356  eulerpartlemgf  34357  ballotlemfc0  34471  ballotlemfcc  34472  ballotlemiex  34480  ballotlemsup  34483  ballotlemsima  34494  ballotlemrv2  34500  ballotth  34516  signsplypnf  34528  signsply0  34529  rpsqrtcn  34571  itgexpif  34584  fsum2dsub  34585  reprfi2  34601  chtvalz  34607  breprexplemc  34610  breprexpnat  34612  circlemeth  34618  circlemethnat  34619  circlevma  34620  circlemethhgt  34621  hgt750lemd  34626  hgt750lema  34635  tgoldbachgtde  34638  tgoldbachgtda  34639  tgoldbachgt  34641  bnj1145  34970  bnj1286  34996  subfacp1lem2a  35148  erdszelem4  35162  erdszelem5  35163  erdszelem7  35165  erdszelem8  35166  kur14lem7  35180  kur14lem9  35182  resconn  35214  iccllysconn  35218  txpss3v  35842  txprel  35843  limitssson  35875  finminlem  36282  tailf  36339  filnetlem3  36344  onint1  36413  bj-unrab  36890  bj-2upln1upl  36988  bj-imdirco  37154  bj-rvecssabl  37270  taupilem2  37286  taupi  37287  poimirlem3  37593  poimirlem30  37620  poimirlem31  37621  poimirlem32  37622  broucube  37624  opnmbllem0  37626  mblfinlem1  37627  mblfinlem2  37628  mblfinlem3  37629  mblfinlem4  37630  ismblfin  37631  mbfposadd  37637  cnambfre  37638  itg2addnc  37644  ftc1cnnclem  37661  ftc1cnnc  37662  ftc1anclem3  37665  ftc1anclem7  37669  ftc1anc  37671  ftc2nc  37672  dvreasin  37676  dvreacos  37677  areacirclem1  37678  areacirclem2  37679  areacirc  37683  caures  37730  reheibor  37809  xrnss3v  38336  xrnrel  38337  atlatmstc  39283  atlatle  39284  pmaple  39726  sspadd1  39780  sspadd2  39781  dvrelog2  42023  dvrelog3  42024  rpsscn  42295  sumcubes  42309  redvmptabs  42350  diophin  42742  4rexfrabdioph  42768  6rexfrabdioph  42769  irrapxlem1  42792  irrapx1  42798  rmxyelqirr  42880  monotuz  42912  jm2.27dlem5  42984  hbtlem2  43095  algbase  43145  algaddg  43146  algmulr  43147  algsca  43148  algvsca  43149  arearect  43186  areaquad  43187  rtrclex  43588  trclubgNEW  43589  trclexi  43591  rtrclexi  43592  cnvtrcl0  43597  dfrtrcl5  43600  trrelsuperrel2dg  43642  relexpaddss  43689  brtrclfv2  43698  frege131d  43735  xphe  43752  clsk3nimkb  44011  gneispace  44105  k0004val0  44125  inaex  44269  lhe4.4ex1a  44301  uzmptshftfval  44318  binomcxplemdvbinom  44325  binomcxplemcvg  44326  binomcxplemnotnn0  44328  relopabVD  44873  dmwf  44938  rnwf  44939  fzisoeu  45277  fzsscn  45288  fzssre  45291  fzossuz  45356  zssxr  45372  uzssre2  45382  supminfxr  45439  uzsscn  45450  rpssxr  45455  uzinico  45536  limcresiooub  45619  limcresioolb  45620  limcleqr  45621  limclner  45628  limclr  45632  limsupequzmpt2  45695  liminfval2  45745  liminfequzmpt2  45768  icccncfext  45864  cncficcgt0  45865  ioodvbdlimc1lem2  45909  ioodvbdlimc2lem  45911  dvnprodlem2  45924  itgsin0pilem1  45927  itgsinexplem1  45931  itgsinexp  45932  dirkercncflem2  46081  fourierdlem16  46100  fourierdlem18  46102  fourierdlem20  46104  fourierdlem21  46105  fourierdlem22  46106  fourierdlem25  46109  fourierdlem37  46121  fourierdlem42  46126  fourierdlem50  46133  fourierdlem52  46135  fourierdlem62  46145  fourierdlem64  46147  fourierdlem66  46149  fourierdlem68  46151  fourierdlem74  46157  fourierdlem75  46158  fourierdlem76  46159  fourierdlem79  46162  fourierdlem83  46166  fourierdlem95  46178  fourierdlem101  46184  fourierdlem102  46185  fourierdlem103  46186  fourierdlem104  46187  fourierdlem112  46195  fourierdlem114  46197  sqwvfoura  46205  sqwvfourb  46206  fouriersw  46208  etransclem24  46235  etransclem48  46259  sge0sn  46356  sge0tsms  46357  sge0f1o  46359  sge0pr  46371  sge0resplit  46383  sge0split  46386  sge0iunmptlemre  46392  sge0isummpt2  46409  carageniuncllem1  46498  hoicvr  46525  hoicvrrex  46533  hoidmvlelem2  46573  hspmbl  46606  smfmullem4  46771  lamberte  46868  rehalfge1  47312  prmdvdsfmtnof1lem1  47546  prmdvdsfmtnof  47548  upgrimpthslem2  47869  upgrimpths  47870  oddibas  48096  2zrngbas  48165  2zrng0  48167  dmtposss  48799  tposres3  48804  sepfsepc  48850  aacllem  49613  amgmlemALT  49615