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

This proof depends on syntax axioms:   ⊆ wss 3906

This proof depends on axioms:  ax-mp 5  ax-1 6  ax-2 7  ax-3 8  ax-gen 1828  ax-4 1842

This proof depends on definitions:  df-bi 210  df-ss 3923

This theorem is used by:  snsstp1  4784  snsstp2  4785  uniintsn  4952  elopabran  5548  ssrnres  6178  cossxp  6276  foimacnv  6842  ssimaex  6970  riotassuni  7413  oprabss  7524  dmexg  7900  rnexg  7901  mptmpoopabbrd  8080  fparlem3  8111  fparlem4  8112  snopsuppss  8177  tposssxp  8228  naddunif  8682  naddasslem1  8683  naddasslem2  8684  mapsspw  8878  sbthlem5  9082  sbthlem7  9084  cnvimamptfin  9313  marypha1lem  9396  ordtypelem4  9486  hartogslem1  9507  ttrclco  9690  cottrcl  9691  tc2  9712  frmin  9724  frrlem16  9733  tz9.12lem1  9762  rankval4  9842  rankxpl  9850  rankmapu  9853  rankxplim  9854  djuin  9916  infxpenlem  10009  ackbij1lem18  10231  cflm  10244  fin23lem29  10336  hsmexlem4  10424  hsmexlem5  10425  brdom3  10523  brdom5  10524  brdom4  10525  smobeth  10582  pwfseqlem3  10656  wundm  10724  wunrn  10725  wunex2  10734  ltsopi  10884  dmaddpi  10886  dmmulpi  10887  nqerf  10926  ltrelxr  11281  uzssre  12895  uzwo2  12947  infssuzle  12966  infssuzcl  12967  uzwo3  12978  nn0ssq  12992  nnssq  12993  qsscn  12995  rpnnen1lem3  13014  rpnnen1lem5  13016  dflt2  13184  ioosscn  13446  unitsscn  13538  fzval2  13549  fzossz  13720  fzossnn  13752  injresinj  13832  flval3  13861  uzsup  13909  uzrdgfni  14007  expcl2lem  14122  rpexpcl  14129  expge0  14147  expge1  14148  hashxrcl  14406  seqcoll  14514  xptrrel  15036  trclublem  15051  01sqrexlem3  15314  limsupval2  15550  limsupgre  15551  rlimpm  15570  rlimclim  15616  isercolllem1  15735  isercolllem2  15736  isercoll  15738  caurcvg  15747  caucvg  15749  summolem2a  15784  summolem2  15785  zsum  15787  fsumcvg3  15798  fsumrpcl  15806  fsumge0  15865  climfsum  15890  ackbijnn  15900  prodmolem2a  16006  prodmolem2  16007  zprod  16009  fprodrpcl  16028  fprodge0  16065  fprodge1  16067  rprisefaccl  16095  divalglem8  16475  sadaddlem  16541  lcmfval  16696  isprm3  16758  maxprmfct  16785  pclem  16915  prmreclem1  16993  prmreclem2  16994  prmreclem3  16995  1arith  17004  4sqlem11  17032  ramtlecl  17077  ramcl2lem  17086  ramxrcl  17094  prmgaplem3  17130  prmgaplem4  17131  cshwshashlem1  17172  structfn  17233  strleun  17234  ressbasss  17316  ressbasss2  17318  srngbase  17380  srngplusg  17381  srngmulr  17382  lmodbase  17396  lmodplusg  17397  lmodsca  17398  ipsbase  17407  ipsaddg  17408  ipsmulr  17409  ipssca  17410  ipsvsca  17411  ipsip  17412  phlbase  17417  phlplusg  17418  phlsca  17419  phlvsca  17420  phlip  17421  odrngbas  17474  odrngplusg  17475  odrngmulr  17476  odrngtset  17477  odrngle  17478  odrngds  17479  prdsvallem  17524  prdsval  17525  prdssca  17526  prdsbas  17527  prdsplusg  17528  prdsmulr  17529  prdsvsca  17530  prdsip  17531  prdsle  17532  prdsds  17534  prdstset  17536  prdshom  17537  prdsco  17538  imasbas  17583  imasds  17584  imasplusg  17588  imasmulr  17589  imassca  17590  imasvsca  17591  imasip  17592  imastset  17593  imasle  17594  wunfunc  17975  fullfunc  17982  fthfunc  17983  isfull  17986  isfth  17990  wunnat  18033  dmcoass  18140  catcisolem  18184  catciso  18185  catcoppccl  18191  catcfuccl  18192  catcxpccl  18280  ipobas  18604  ipolerval  18605  ipotset  18606  psdmrn  18646  psss  18653  ledm  18663  lern  18664  dirdm  18673  dirge  18676  mulgfval  19158  mvdco  19538  f1omvdconj  19539  gexex  19946  gsumval3  20000  lssacs  21117  cnfldbas  21555  mpocnfldadd  21556  mpocnfldmul  21558  cnfldcj  21560  cnfldtset  21561  cnfldle  21562  cnfldds  21563  cnfldunif  21564  rge0srg  21617  zntoslem  21735  asplss  22052  aspsubrg  22054  psrass1lem  22112  psrbas  22113  psrplusg  22116  psrmulr  22121  psrsca  22126  psrvscafval  22127  psrass1  22142  psrass23l  22145  psrcom  22146  psrass23  22147  psropprmul  22426  coe1mul2  22459  ofco2  22637  toponsspwpw  23108  dmtopon  23109  leordtval2  23398  lmbrf  23446  lmres  23486  fiuncmp  23590  comppfsc  23718  1stckgenlem  23739  kgencn3  23744  ptbasfi  23767  xkoopn  23775  txcnmpt  23810  txkgen  23838  opnfbas  24028  fmfnfmlem4  24143  tsmsxplem1  24339  trust  24415  restutop  24423  nmoffn  24897  nmofval  24900  nmogelb  24902  nmolb  24903  nmof  24905  qtopbas  24945  tgqioo  24986  re2ndc  24987  iitopon  25067  dfii3  25071  cnheiborlem  25142  bndth  25146  lebnumii  25154  pcoass  25212  cphsqrtcl  25372  lmmbrf  25450  iscauf  25468  caucfil  25471  lmclimf  25492  rrxmval  25593  rrxmet  25596  ovolfioo  25655  ovolficc  25656  ovolficcss  25657  ovolfsf  25659  ovollb  25667  ovolicc2lem3  25707  ovolicc2lem4  25708  ovolicc2  25710  volf  25717  volsup  25744  ovolfs2  25759  uniiccdif  25766  uniioovol  25767  uniiccvol  25768  uniioombllem2  25771  uniioombllem3a  25772  uniioombllem3  25773  uniioombllem4  25774  uniioombllem5  25775  uniioombl  25777  dyadmbllem  25787  dyadmbl  25788  opnmbllem  25789  opnmblALT  25791  volsup2  25793  vitalilem4  25799  vitalilem5  25800  vitali  25801  mbfimaopnlem  25843  mbflimsup  25854  i1f0  25875  i1f1  25878  itg11  25879  itg2mulc  25935  itg2gt0  25948  ellimc2  26065  limcresi  26073  dvreslem  26097  dvres2lem  26098  dvaddbr  26126  dvmulbr  26127  dvlipcn  26182  c1liplem1  26184  lhop1lem  26201  lhop1  26202  lhop2  26203  lhop  26204  dvfsumrlim  26219  ftc1cn  26231  itgsubstlem  26236  itgsubst  26237  itgpowd  26238  mdegleb  26250  mdeglt  26251  mdegldg  26252  mdegxrcl  26253  mdegcl  26255  mdegaddle  26260  mdegmullem  26264  deg1mul3le  26303  ig1peu  26361  ig1pdvds  26366  aacjcl  26519  aannenlem2  26521  aannenlem3  26522  aalioulem2  26525  taylfval  26551  radcnvcl  26609  radcnvlt1  26610  radcnvle  26612  abelth  26633  abelth2  26634  pilem2  26644  pilem3  26645  pige3ALT  26714  recosf1o  26729  resinf1o  26730  tanord1  26731  logcn  26841  dvlog  26845  dvlog2lem  26846  efopn  26852  logtayl  26854  cxpcn3  26942  loglesqrt  26955  ssscongptld  27016  leibpi  27136  efrlim  27163  jensenlem1  27180  jensenlem2  27181  jensen  27182  amgm  27184  lgamgulmlem2  27223  ftalem5  27270  efnnfsumcl  27296  efchtdvds  27352  mpodvdsmulf1o  27387  fsumdvdsmul  27388  dvdsmulf1o  27389  lgsfcl2  27496  2sqlem6  27616  2sqlem8  27619  2sqlem9  27620  rpvmasumlem  27680  rpvmasum2  27705  dchrisum0re  27706  dchrisum0lem3  27712  dchrisum0  27713  rplogsum  27720  dirith2  27721  noextendseq  27860  oldf  28059  leftssno  28095  rightssno  28096  addbdaylem  28239  mulsproplem12  28349  mulsproplem13  28350  mulsproplem14  28351  mulsasslem3  28387  precsexlem11  28439  oncutlt  28486  bdayons  28498  nnssno  28544  axtgcgrrflx  28760  axtgcgrid  28761  axtgsegcon  28762  axtg5seg  28763  axtgbtwnid  28764  axtgpasch  28765  axtgcont1  28766  tgcgr4  28829  motcgrg  28842  tglng  28844  upgrss  29467  pthdivtx  30105  disjxwwlkn  30291  ex-fpar  30842  nmlno0lem  31174  hlimcaui  31617  chsspwh  31628  shsss  31694  chintcli  31712  shsleji  31751  shub1i  31755  shsval2i  31768  lejdii  31919  spanuni  31925  sshhococi  31927  spansnpji  31959  osumcori  32024  5oai  32042  3oalem6  32048  3oai  32049  pjssmii  32062  mayete3i  32109  mayetes3i  32110  nmlnop0iALT  32376  imaelshi  32439  pjnmopi  32529  pjclem1  32576  pjci  32581  mdslmd1lem1  32706  shatomistici  32742  hatomistici  32743  chpssati  32744  xppreima  33019  iundisjfi  33170  iundisj2fi  33171  fprodex01  33198  indsumin  33210  xrsmulgzz  33352  fsumrp0cl  33364  gsummpt2co  33391  cycpmfv2  33457  cycpmrn  33486  rlocbas  33611  rlocaddval  33612  rlocmulval  33613  1fldgenq  33666  xrge0slmod  33691  lsmsnorb  33727  idlsrgbas  33817  idlsrgplusg  33818  idlsrgmulr  33820  idlsrgtset  33821  selvply1rhmlemb  33932  esplyind  33988  vietalem  33992  constrextdg2  34162  ordtconnlem1  34337  xrge0iifhom  34350  lmlimxrge0  34361  lmxrge0  34365  esumcst  34476  esumpfinvallem  34487  esumpfinval  34488  esumpfinvalf  34489  esumcvg  34499  imambfm  34676  elmbfmvol2  34681  sxbrsigalem3  34686  sxbrsigalem2  34700  sxbrsigalem4  34701  sitgclg  34756  eulerpartlem1  34781  eulerpartlemgvv  34790  eulerpartlemgh  34792  eulerpartlemgf  34793  ballotlemfc0  34907  ballotlemfcc  34908  ballotlemiex  34916  ballotlemsup  34919  ballotlemsima  34930  ballotlemrv2  34936  ballotth  34952  signsplypnf  34961  signsply0  34962  rpsqrtcn  35004  itgexpif  35017  fsum2dsub  35018  reprfi2  35034  chtvalz  35040  breprexplemc  35043  breprexpnat  35045  circlemeth  35051  circlemethnat  35052  circlevma  35053  circlemethhgt  35054  hgt750lemd  35059  hgt750lema  35068  tgoldbachgtde  35071  tgoldbachgtda  35072  tgoldbachgt  35074  bnj1145  35405  bnj1286  35431  subfacp1lem2a  35685  erdszelem4  35699  erdszelem5  35700  erdszelem7  35702  erdszelem8  35703  kur14lem7  35717  kur14lem9  35719  resconn  35751  iccllysconn  35755  txpss3v  36381  txprel  36382  limitssson  36414  finminlem  36862  tailf  36919  filnetlem3  36924  onint1  36993  ttcuniun  37054  bj-unrab  37595  bj-2upln1upl  37693  bj-imdirco  37867  bj-rvecssabl  37983  taupilem2  37999  taupi  38000  poimirlem3  38307  poimirlem30  38334  poimirlem31  38335  poimirlem32  38336  broucube  38338  opnmbllem0  38340  mblfinlem1  38341  mblfinlem2  38342  mblfinlem3  38343  mblfinlem4  38344  ismblfin  38345  mbfposadd  38351  cnambfre  38352  itg2addnc  38358  ftc1cnnclem  38375  ftc1cnnc  38376  ftc1anclem3  38379  ftc1anclem7  38383  ftc1anc  38385  ftc2nc  38386  dvreasin  38390  dvreacos  38391  areacirclem1  38392  areacirclem2  38393  areacirc  38397  caures  38444  reheibor  38523  xrnss3v  39063  xrnrel  39064  atlatmstc  40126  atlatle  40127  pmaple  40568  sspadd1  40622  sspadd2  40623  dvrelog2  42864  dvrelog3  42865  rpsscn  43093  sumcubes  43107  redvmptabs  43154  diophin  43536  4rexfrabdioph  43558  6rexfrabdioph  43559  irrapxlem1  43582  irrapx1  43588  rmxyelqirr  43670  monotuz  43701  jm2.27dlem5  43773  hbtlem2  43884  algbase  43934  algaddg  43935  algmulr  43936  algsca  43937  algvsca  43938  arearect  43975  areaquad  43976  rtrclex  44376  trclubgNEW  44377  trclexi  44379  rtrclexi  44380  cnvtrcl0  44385  dfrtrcl5  44388  trrelsuperrel2dg  44430  relexpaddss  44477  brtrclfv2  44486  frege131d  44523  xphe  44540  clsk3nimkb  44799  gneispace  44893  k0004val0  44913  inaex  45040  lhe4.4ex1a  45072  uzmptshftfval  45089  binomcxplemdvbinom  45096  binomcxplemcvg  45097  binomcxplemnotnn0  45099  relopabVD  45642  dmwf  45707  rnwf  45708  fzisoeu  46052  fzsscn  46063  fzssre  46066  fzossuz  46129  zssxr  46145  uzssre2  46154  supminfxr  46211  uzsscn  46222  rpssxr  46227  uzinico  46308  limcresiooub  46389  limcresioolb  46390  limcleqr  46391  limclner  46398  limclr  46402  limsupequzmpt2  46465  liminfval2  46515  liminfequzmpt2  46538  icccncfext  46634  cncficcgt0  46635  ioodvbdlimc1lem2  46679  ioodvbdlimc2lem  46681  dvnprodlem2  46694  itgsin0pilem1  46697  itgsinexplem1  46701  itgsinexp  46702  dirkercncflem2  46851  fourierdlem16  46870  fourierdlem18  46872  fourierdlem20  46874  fourierdlem21  46875  fourierdlem22  46876  fourierdlem25  46879  fourierdlem37  46891  fourierdlem42  46896  fourierdlem50  46903  fourierdlem52  46905  fourierdlem62  46915  fourierdlem64  46917  fourierdlem66  46919  fourierdlem68  46921  fourierdlem74  46927  fourierdlem75  46928  fourierdlem76  46929  fourierdlem79  46932  fourierdlem83  46936  fourierdlem95  46948  fourierdlem101  46954  fourierdlem102  46955  fourierdlem103  46956  fourierdlem104  46957  fourierdlem112  46965  fourierdlem114  46967  sqwvfoura  46975  sqwvfourb  46976  fouriersw  46978  etransclem24  47005  etransclem48  47029  sge0sn  47126  sge0tsms  47127  sge0f1o  47129  sge0pr  47141  sge0resplit  47153  sge0split  47156  sge0iunmptlemre  47162  sge0isummpt2  47179  carageniuncllem1  47268  hoicvr  47295  hoicvrrex  47303  hoidmvlelem2  47343  hspmbl  47376  smfmullem4  47541  chnsuslle  47630  lamberte  47658  rehalfge1  48109  prmdvdsfmtnof1lem1  48369  prmdvdsfmtnof  48371  upgrimpthslem2  48706  upgrimpths  48707  oddibas  48971  2zrngbas  49040  2zrng0  49042  dmtposss  49687  tposres3  49692  sepfsepc  49739  uptrlem1  50021  uptrlem2  50022  uptrlem3  50023  uptra  50026  uptrar  50027  uobeqw  50030  uptr2  50032  uptr2a  50033  fucoppcfunc  50223  aacllem  50654  amgmlemALT  50684