Theorem sstri 3947

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

Syntax hints:   ⊆ wss 3905

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 3922

This theorem is referenced by:  snsstp1  4770  snsstp2  4771  uniintsn  4938  elopabran  5508  ssrnres  6131  cossxp  6224  foimacnv  6785  ssimaex  6912  riotassuni  7350  oprabss  7461  dmexg  7841  rnexg  7842  fabexgOLD  7879  mptmpoopabbrd  8022  fparlem3  8054  fparlem4  8055  snopsuppss  8119  tposssxp  8170  naddunif  8618  naddasslem1  8619  naddasslem2  8620  mapsspw  8812  sbthlem5  9015  sbthlem7  9017  cnvimamptfin  9262  marypha1lem  9342  ordtypelem4  9432  hartogslem1  9453  ttrclco  9633  cottrcl  9634  tc2  9657  frmin  9664  frrlem16  9673  tz9.12lem1  9702  rankval4  9782  rankxpl  9790  rankmapu  9793  rankxplim  9794  djuin  9833  infxpenlem  9926  ackbij1lem18  10149  cflm  10163  fin23lem29  10254  hsmexlem4  10342  hsmexlem5  10343  brdom3  10441  brdom5  10442  brdom4  10443  smobeth  10499  pwfseqlem3  10573  wundm  10641  wunrn  10642  wunex2  10651  ltsopi  10801  dmaddpi  10803  dmmulpi  10804  nqerf  10843  ltrelxr  11195  uzssre  12775  uzwo2  12831  infssuzle  12850  infssuzcl  12851  uzwo3  12862  nn0ssq  12876  nnssq  12877  qsscn  12879  rpnnen1lem3  12898  rpnnen1lem5  12900  dflt2  13068  ioosscn  13329  unitsscn  13421  fzval2  13431  fzossz  13600  fzossnn  13632  injresinj  13709  flval3  13737  uzsup  13785  uzrdgfni  13883  expcl2lem  13998  rpexpcl  14005  expge0  14023  expge1  14024  hashxrcl  14282  seqcoll  14389  xptrrel  14905  trclublem  14920  01sqrexlem3  15169  limsupval2  15405  limsupgre  15406  rlimpm  15425  rlimclim  15471  isercolllem1  15590  isercolllem2  15591  isercoll  15593  caurcvg  15602  caucvg  15604  summolem2a  15640  summolem2  15641  zsum  15643  fsumcvg3  15654  fsumrpcl  15662  fsumge0  15720  climfsum  15745  ackbijnn  15753  prodmolem2a  15859  prodmolem2  15860  zprod  15862  fprodrpcl  15881  fprodge0  15918  fprodge1  15920  rprisefaccl  15948  divalglem8  16329  sadaddlem  16395  lcmfval  16550  isprm3  16612  maxprmfct  16638  pclem  16768  prmreclem1  16846  prmreclem2  16847  prmreclem3  16848  1arith  16857  4sqlem11  16885  ramtlecl  16930  ramcl2lem  16939  ramxrcl  16947  prmgaplem3  16983  prmgaplem4  16984  cshwshashlem1  17025  structfn  17085  strleun  17086  ressbasss  17168  ressbasss2  17170  srngbase  17232  srngplusg  17233  srngmulr  17234  lmodbase  17248  lmodplusg  17249  lmodsca  17250  ipsbase  17259  ipsaddg  17260  ipsmulr  17261  ipssca  17262  ipsvsca  17263  ipsip  17264  phlbase  17269  phlplusg  17270  phlsca  17271  phlvsca  17272  phlip  17273  odrngbas  17326  odrngplusg  17327  odrngmulr  17328  odrngtset  17329  odrngle  17330  odrngds  17331  prdsvallem  17376  prdsval  17377  prdssca  17378  prdsbas  17379  prdsplusg  17380  prdsmulr  17381  prdsvsca  17382  prdsip  17383  prdsle  17384  prdsds  17386  prdstset  17388  prdshom  17389  prdsco  17390  imasbas  17434  imasds  17435  imasplusg  17439  imasmulr  17440  imassca  17441  imasvsca  17442  imasip  17443  imastset  17444  imasle  17445  wunfunc  17826  fullfunc  17833  fthfunc  17834  isfull  17837  isfth  17841  wunnat  17884  dmcoass  17991  catcisolem  18035  catciso  18036  catcoppccl  18042  catcfuccl  18043  catcxpccl  18131  ipobas  18455  ipolerval  18456  ipotset  18457  psdmrn  18497  psss  18504  ledm  18514  lern  18515  dirdm  18524  dirge  18527  mulgfval  18966  mvdco  19342  f1omvdconj  19343  gexex  19750  gsumval3  19804  lssacs  20888  cnfldbas  21283  mpocnfldadd  21284  mpocnfldmul  21286  cnfldcj  21288  cnfldtset  21289  cnfldle  21290  cnfldds  21291  cnfldunif  21292  cnfldbasOLD  21298  cnfldaddOLD  21299  cnfldmulOLD  21300  cnfldcjOLD  21301  cnfldtsetOLD  21302  cnfldleOLD  21303  cnflddsOLD  21304  cnfldunifOLD  21305  rge0srg  21363  zntoslem  21481  asplss  21799  aspsubrg  21801  psrass1lem  21857  psrbas  21858  psrplusg  21861  psrmulr  21867  psrsca  21872  psrvscafval  21873  psrass1  21889  psrass23l  21892  psrcom  21893  psrass23  21894  psropprmul  22138  coe1mul2  22171  ofco2  22354  toponsspwpw  22825  dmtopon  22826  leordtval2  23115  lmbrf  23163  lmres  23203  fiuncmp  23307  comppfsc  23435  1stckgenlem  23456  kgencn3  23461  ptbasfi  23484  xkoopn  23492  txcnmpt  23527  txkgen  23555  opnfbas  23745  fmfnfmlem4  23860  tsmsxplem1  24056  trust  24133  restutop  24141  nmoffn  24615  nmofval  24618  nmogelb  24620  nmolb  24621  nmof  24623  qtopbas  24663  tgqioo  24704  re2ndc  24705  iitopon  24788  dfii3  24792  iimulcnOLD  24851  cnheiborlem  24869  bndth  24873  lebnumii  24881  reparphtiOLD  24913  pcoass  24940  cphsqrtcl  25100  lmmbrf  25178  iscauf  25196  caucfil  25199  lmclimf  25220  rrxmval  25321  rrxmet  25324  ovolfioo  25384  ovolficc  25385  ovolficcss  25386  ovolfsf  25388  ovollb  25396  ovolicc2lem3  25436  ovolicc2lem4  25437  ovolicc2  25439  volf  25446  volsup  25473  ovolfs2  25488  uniiccdif  25495  uniioovol  25496  uniiccvol  25497  uniioombllem2  25500  uniioombllem3a  25501  uniioombllem3  25502  uniioombllem4  25503  uniioombllem5  25504  uniioombl  25506  dyadmbllem  25516  dyadmbl  25517  opnmbllem  25518  opnmblALT  25520  volsup2  25522  vitalilem4  25528  vitalilem5  25529  vitali  25530  mbfimaopnlem  25572  mbflimsup  25583  i1f0  25604  i1f1  25607  itg11  25608  itg2mulc  25664  itg2gt0  25677  ellimc2  25794  limcresi  25802  dvreslem  25826  dvres2lem  25827  dvaddbr  25856  dvmulbr  25857  dvmulbrOLD  25858  dvlipcn  25915  c1liplem1  25917  lhop1lem  25934  lhop1  25935  lhop2  25936  lhop  25937  dvfsumrlim  25954  ftc1cn  25966  itgsubstlem  25971  itgsubst  25972  itgpowd  25973  mdegleb  25985  mdeglt  25986  mdegldg  25987  mdegxrcl  25988  mdegcl  25990  mdegaddle  25995  mdegmullem  25999  deg1mul3le  26038  ig1peu  26096  ig1pdvds  26101  aacjcl  26251  aannenlem2  26253  aannenlem3  26254  aalioulem2  26257  taylfval  26282  radcnvcl  26342  radcnvlt1  26343  radcnvle  26345  abelth  26367  abelth2  26368  pilem2  26378  pilem3  26379  pige3ALT  26445  recosf1o  26460  resinf1o  26461  tanord1  26462  logcn  26572  dvlog  26576  dvlog2lem  26577  efopn  26583  logtayl  26585  cxpcn3  26674  loglesqrt  26687  ssscongptld  26748  leibpi  26868  efrlim  26895  efrlimOLD  26896  jensenlem1  26913  jensenlem2  26914  jensen  26915  amgm  26917  lgamgulmlem2  26956  ftalem5  27003  efnnfsumcl  27029  efchtdvds  27085  mpodvdsmulf1o  27120  fsumdvdsmul  27121  dvdsmulf1o  27122  fsumdvdsmulOLD  27123  lgsfcl2  27230  2sqlem6  27350  2sqlem8  27353  2sqlem9  27354  rpvmasumlem  27414  rpvmasum2  27439  dchrisum0re  27440  dchrisum0lem3  27446  dchrisum0  27447  rplogsum  27454  dirith2  27455  noextendseq  27595  oldf  27785  leftssno  27813  rightssno  27814  addsbdaylem  27946  mulsproplem12  28053  mulsproplem13  28054  mulsproplem14  28055  mulsasslem3  28091  precsexlem11  28142  onscutlt  28188  bdayon  28196  nnssno  28238  axtgcgrrflx  28425  axtgcgrid  28426  axtgsegcon  28427  axtg5seg  28428  axtgbtwnid  28429  axtgpasch  28430  axtgcont1  28431  tgcgr4  28494  motcgrg  28507  tglng  28509  upgrss  29051  pthdivtx  29690  disjxwwlkn  29876  ex-fpar  30424  nmlno0lem  30755  hlimcaui  31198  chsspwh  31209  shsss  31275  chintcli  31293  shsleji  31332  shub1i  31336  shsval2i  31349  lejdii  31500  spanuni  31506  sshhococi  31508  spansnpji  31540  osumcori  31605  5oai  31623  3oalem6  31629  3oai  31630  pjssmii  31643  mayete3i  31690  mayetes3i  31691  nmlnop0iALT  31957  imaelshi  32020  pjnmopi  32110  pjclem1  32157  pjci  32162  mdslmd1lem1  32287  shatomistici  32323  hatomistici  32324  chpssati  32325  xppreima  32602  iundisjfi  32752  iundisj2fi  32753  fprodex01  32783  indsumin  32818  xrsmulgzz  32976  fsumrp0cl  32988  gsummpt2co  33014  cycpmfv2  33069  cycpmrn  33098  rlocbas  33220  rlocaddval  33221  rlocmulval  33222  1fldgenq  33274  xrge0slmod  33298  lsmsnorb  33341  idlsrgbas  33454  idlsrgplusg  33455  idlsrgmulr  33457  idlsrgtset  33458  constrextdg2  33718  ordtconnlem1  33893  xrge0iifhom  33906  lmlimxrge0  33917  lmxrge0  33921  esumcst  34032  esumpfinvallem  34043  esumpfinval  34044  esumpfinvalf  34045  esumcvg  34055  imambfm  34232  elmbfmvol2  34237  sxbrsigalem3  34242  sxbrsigalem2  34256  sxbrsigalem4  34257  sitgclg  34312  eulerpartlem1  34337  eulerpartlemgvv  34346  eulerpartlemgh  34348  eulerpartlemgf  34349  ballotlemfc0  34463  ballotlemfcc  34464  ballotlemiex  34472  ballotlemsup  34475  ballotlemsima  34486  ballotlemrv2  34492  ballotth  34508  signsplypnf  34520  signsply0  34521  rpsqrtcn  34563  itgexpif  34576  fsum2dsub  34577  reprfi2  34593  chtvalz  34599  breprexplemc  34602  breprexpnat  34604  circlemeth  34610  circlemethnat  34611  circlevma  34612  circlemethhgt  34613  hgt750lemd  34618  hgt750lema  34627  tgoldbachgtde  34630  tgoldbachgtda  34631  tgoldbachgt  34633  bnj1145  34962  bnj1286  34988  subfacp1lem2a  35155  erdszelem4  35169  erdszelem5  35170  erdszelem7  35172  erdszelem8  35173  kur14lem7  35187  kur14lem9  35189  resconn  35221  iccllysconn  35225  txpss3v  35854  txprel  35855  limitssson  35887  finminlem  36294  tailf  36351  filnetlem3  36356  onint1  36425  bj-unrab  36902  bj-2upln1upl  37000  bj-imdirco  37166  bj-rvecssabl  37282  taupilem2  37298  taupi  37299  poimirlem3  37605  poimirlem30  37632  poimirlem31  37633  poimirlem32  37634  broucube  37636  opnmbllem0  37638  mblfinlem1  37639  mblfinlem2  37640  mblfinlem3  37641  mblfinlem4  37642  ismblfin  37643  mbfposadd  37649  cnambfre  37650  itg2addnc  37656  ftc1cnnclem  37673  ftc1cnnc  37674  ftc1anclem3  37677  ftc1anclem7  37681  ftc1anc  37683  ftc2nc  37684  dvreasin  37688  dvreacos  37689  areacirclem1  37690  areacirclem2  37691  areacirc  37695  caures  37742  reheibor  37821  xrnss3v  38342  xrnrel  38343  atlatmstc  39300  atlatle  39301  pmaple  39743  sspadd1  39797  sspadd2  39798  dvrelog2  42040  dvrelog3  42041  rpsscn  42275  sumcubes  42289  redvmptabs  42336  diophin  42748  4rexfrabdioph  42774  6rexfrabdioph  42775  irrapxlem1  42798  irrapx1  42804  rmxyelqirr  42886  monotuz  42917  jm2.27dlem5  42989  hbtlem2  43100  algbase  43150  algaddg  43151  algmulr  43152  algsca  43153  algvsca  43154  arearect  43191  areaquad  43192  rtrclex  43593  trclubgNEW  43594  trclexi  43596  rtrclexi  43597  cnvtrcl0  43602  dfrtrcl5  43605  trrelsuperrel2dg  43647  relexpaddss  43694  brtrclfv2  43703  frege131d  43740  xphe  43757  clsk3nimkb  44016  gneispace  44110  k0004val0  44130  inaex  44273  lhe4.4ex1a  44305  uzmptshftfval  44322  binomcxplemdvbinom  44329  binomcxplemcvg  44330  binomcxplemnotnn0  44332  relopabVD  44877  dmwf  44942  rnwf  44943  fzisoeu  45285  fzsscn  45296  fzssre  45299  fzossuz  45364  zssxr  45380  uzssre2  45390  supminfxr  45447  uzsscn  45458  rpssxr  45463  uzinico  45544  limcresiooub  45627  limcresioolb  45628  limcleqr  45629  limclner  45636  limclr  45640  limsupequzmpt2  45703  liminfval2  45753  liminfequzmpt2  45776  icccncfext  45872  cncficcgt0  45873  ioodvbdlimc1lem2  45917  ioodvbdlimc2lem  45919  dvnprodlem2  45932  itgsin0pilem1  45935  itgsinexplem1  45939  itgsinexp  45940  dirkercncflem2  46089  fourierdlem16  46108  fourierdlem18  46110  fourierdlem20  46112  fourierdlem21  46113  fourierdlem22  46114  fourierdlem25  46117  fourierdlem37  46129  fourierdlem42  46134  fourierdlem50  46141  fourierdlem52  46143  fourierdlem62  46153  fourierdlem64  46155  fourierdlem66  46157  fourierdlem68  46159  fourierdlem74  46165  fourierdlem75  46166  fourierdlem76  46167  fourierdlem79  46170  fourierdlem83  46174  fourierdlem95  46186  fourierdlem101  46192  fourierdlem102  46193  fourierdlem103  46194  fourierdlem104  46195  fourierdlem112  46203  fourierdlem114  46205  sqwvfoura  46213  sqwvfourb  46214  fouriersw  46216  etransclem24  46243  etransclem48  46267  sge0sn  46364  sge0tsms  46365  sge0f1o  46367  sge0pr  46379  sge0resplit  46391  sge0split  46394  sge0iunmptlemre  46400  sge0isummpt2  46417  carageniuncllem1  46506  hoicvr  46533  hoicvrrex  46541  hoidmvlelem2  46581  hspmbl  46614  smfmullem4  46779  lamberte  46876  rehalfge1  47323  prmdvdsfmtnof1lem1  47572  prmdvdsfmtnof  47574  upgrimpthslem2  47896  upgrimpths  47897  oddibas  48161  2zrngbas  48230  2zrng0  48232  dmtposss  48864  tposres3  48869  sepfsepc  48916  uptrlem1  49199  uptrlem2  49200  uptrlem3  49201  uptra  49204  uptrar  49205  uobeqw  49208  uptr2  49210  uptr2a  49211  fucoppcfunc  49401  aacllem  49790  amgmlemALT  49792