Theorem sstri 4004

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

Syntax hints:   ⊆ wss 3962

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

This theorem depends on definitions:  df-bi 207  df-ss 3979

This theorem is referenced by:  snsstp1  4820  snsstp2  4821  uniintsn  4989  elopabran  5571  ssrnres  6199  cossxp  6293  foimacnv  6865  ssimaex  6993  riotassuni  7427  oprabss  7539  dmexg  7923  rnexg  7924  fabexgOLD  7959  mptmpoopabbrd  8103  fparlem3  8137  fparlem4  8138  snopsuppss  8202  tposssxp  8253  naddunif  8729  naddasslem1  8730  naddasslem2  8731  mapsspw  8916  sbthlem5  9125  sbthlem7  9127  cnvimamptfin  9390  marypha1lem  9470  ordtypelem4  9558  hartogslem1  9579  ttrclco  9755  cottrcl  9756  tc2  9779  frmin  9786  frrlem16  9795  tz9.12lem1  9824  rankval4  9904  rankxpl  9912  rankmapu  9915  rankxplim  9916  djuin  9955  infxpenlem  10050  ackbij1lem18  10273  cflm  10287  fin23lem29  10378  hsmexlem4  10466  hsmexlem5  10467  brdom3  10565  brdom5  10566  brdom4  10567  smobeth  10623  pwfseqlem3  10697  wundm  10765  wunrn  10766  wunex2  10775  ltsopi  10925  dmaddpi  10927  dmmulpi  10928  nqerf  10967  ltrelxr  11319  uzssre  12897  uzwo2  12951  infssuzle  12970  infssuzcl  12971  uzwo3  12982  nn0ssq  12996  nnssq  12997  qsscn  12999  rpnnen1lem3  13018  rpnnen1lem5  13020  dflt2  13186  ioosscn  13445  unitsscn  13536  fzval2  13546  fzossz  13715  fzossnn  13747  injresinj  13823  flval3  13851  uzsup  13899  uzrdgfni  13995  expcl2lem  14110  rpexpcl  14117  expge0  14135  expge1  14136  hashxrcl  14392  seqcoll  14499  xptrrel  15015  trclublem  15030  01sqrexlem3  15279  limsupval2  15512  limsupgre  15513  rlimpm  15532  rlimclim  15578  isercolllem1  15697  isercolllem2  15698  isercoll  15700  caurcvg  15709  caucvg  15711  summolem2a  15747  summolem2  15748  zsum  15750  fsumcvg3  15761  fsumrpcl  15769  fsumge0  15827  climfsum  15852  ackbijnn  15860  prodmolem2a  15966  prodmolem2  15967  zprod  15969  fprodrpcl  15988  fprodge0  16025  fprodge1  16027  rprisefaccl  16055  divalglem8  16433  sadaddlem  16499  lcmfval  16654  isprm3  16716  maxprmfct  16742  pclem  16871  prmreclem1  16949  prmreclem2  16950  prmreclem3  16951  1arith  16960  4sqlem11  16988  ramtlecl  17033  ramcl2lem  17042  ramxrcl  17050  prmgaplem3  17086  prmgaplem4  17087  cshwshashlem1  17129  structfn  17189  strleun  17190  ressbasss  17283  ressbasss2  17285  srngbase  17355  srngplusg  17356  srngmulr  17357  lmodbase  17371  lmodplusg  17372  lmodsca  17373  ipsbase  17382  ipsaddg  17383  ipsmulr  17384  ipssca  17385  ipsvsca  17386  ipsip  17387  phlbase  17392  phlplusg  17393  phlsca  17394  phlvsca  17395  phlip  17396  odrngbas  17449  odrngplusg  17450  odrngmulr  17451  odrngtset  17452  odrngle  17453  odrngds  17454  prdsvallem  17500  prdsval  17501  prdssca  17502  prdsbas  17503  prdsplusg  17504  prdsmulr  17505  prdsvsca  17506  prdsip  17507  prdsle  17508  prdsds  17510  prdstset  17512  prdshom  17513  prdsco  17514  imasbas  17558  imasds  17559  imasplusg  17563  imasmulr  17564  imassca  17565  imasvsca  17566  imasip  17567  imastset  17568  imasle  17569  wunfunc  17951  wunfuncOLD  17952  fullfunc  17959  fthfunc  17960  isfull  17963  isfth  17967  wunnat  18010  wunnatOLD  18011  dmcoass  18119  catcisolem  18163  catciso  18164  catcoppccl  18170  catcoppcclOLD  18171  catcfuccl  18172  catcfucclOLD  18173  catcxpccl  18262  catcxpcclOLD  18263  ipobas  18588  ipolerval  18589  ipotset  18590  psdmrn  18630  psss  18637  ledm  18647  lern  18648  dirdm  18657  dirge  18660  mulgfval  19099  mvdco  19477  f1omvdconj  19478  gexex  19885  gsumval3  19939  lssacs  20982  cnfldbas  21385  mpocnfldadd  21386  mpocnfldmul  21388  cnfldcj  21390  cnfldtset  21391  cnfldle  21392  cnfldds  21393  cnfldunif  21394  cnfldbasOLD  21400  cnfldaddOLD  21401  cnfldmulOLD  21402  cnfldcjOLD  21403  cnfldtsetOLD  21404  cnfldleOLD  21405  cnflddsOLD  21406  cnfldunifOLD  21407  rge0srg  21473  zntoslem  21592  asplss  21911  aspsubrg  21913  psrass1lem  21969  psrbas  21970  psrplusg  21973  psrmulr  21979  psrsca  21984  psrvscafval  21985  psrass1  22001  psrass23l  22004  psrcom  22005  psrass23  22006  psropprmul  22254  coe1mul2  22287  ofco2  22472  toponsspwpw  22943  dmtopon  22944  leordtval2  23235  lmbrf  23283  lmres  23323  fiuncmp  23427  comppfsc  23555  1stckgenlem  23576  kgencn3  23581  ptbasfi  23604  xkoopn  23612  txcnmpt  23647  txkgen  23675  opnfbas  23865  fmfnfmlem4  23980  tsmsxplem1  24176  trust  24253  restutop  24261  nmoffn  24747  nmofval  24750  nmogelb  24752  nmolb  24753  nmof  24755  qtopbas  24795  tgqioo  24835  re2ndc  24836  iitopon  24918  dfii3  24922  iimulcnOLD  24981  cnheiborlem  24999  bndth  25003  lebnumii  25011  reparphtiOLD  25043  pcoass  25070  cphsqrtcl  25231  lmmbrf  25309  iscauf  25327  caucfil  25330  lmclimf  25351  rrxmval  25452  rrxmet  25455  ovolfioo  25515  ovolficc  25516  ovolficcss  25517  ovolfsf  25519  ovollb  25527  ovolicc2lem3  25567  ovolicc2lem4  25568  ovolicc2  25570  volf  25577  volsup  25604  ovolfs2  25619  uniiccdif  25626  uniioovol  25627  uniiccvol  25628  uniioombllem2  25631  uniioombllem3a  25632  uniioombllem3  25633  uniioombllem4  25634  uniioombllem5  25635  uniioombl  25637  dyadmbllem  25647  dyadmbl  25648  opnmbllem  25649  opnmblALT  25651  volsup2  25653  vitalilem4  25659  vitalilem5  25660  vitali  25661  mbfimaopnlem  25703  mbflimsup  25714  i1f0  25735  i1f1  25738  itg11  25739  itg2mulc  25796  itg2gt0  25809  ellimc2  25926  limcresi  25934  dvreslem  25958  dvres2lem  25959  dvaddbr  25988  dvmulbr  25989  dvmulbrOLD  25990  dvlipcn  26047  c1liplem1  26049  lhop1lem  26066  lhop1  26067  lhop2  26068  lhop  26069  dvfsumrlim  26086  ftc1cn  26098  itgsubstlem  26103  itgsubst  26104  itgpowd  26105  mdegleb  26117  mdeglt  26118  mdegldg  26119  mdegxrcl  26120  mdegcl  26122  mdegaddle  26127  mdegmullem  26131  deg1mul3le  26170  ig1peu  26228  ig1pdvds  26233  aacjcl  26383  aannenlem2  26385  aannenlem3  26386  aalioulem2  26389  taylfval  26414  radcnvcl  26474  radcnvlt1  26475  radcnvle  26477  abelth  26499  abelth2  26500  pilem2  26510  pilem3  26511  pige3ALT  26576  recosf1o  26591  resinf1o  26592  tanord1  26593  logcn  26703  dvlog  26707  dvlog2lem  26708  efopn  26714  logtayl  26716  cxpcn3  26805  loglesqrt  26818  ssscongptld  26879  leibpi  26999  efrlim  27026  efrlimOLD  27027  jensenlem1  27044  jensenlem2  27045  jensen  27046  amgm  27048  lgamgulmlem2  27087  ftalem5  27134  efnnfsumcl  27160  efchtdvds  27216  mpodvdsmulf1o  27251  fsumdvdsmul  27252  dvdsmulf1o  27253  fsumdvdsmulOLD  27254  lgsfcl2  27361  2sqlem6  27481  2sqlem8  27484  2sqlem9  27485  rpvmasumlem  27545  rpvmasum2  27570  dchrisum0re  27571  dchrisum0lem3  27577  dchrisum0  27578  rplogsum  27585  dirith2  27586  noextendseq  27726  oldf  27910  leftssno  27933  rightssno  27934  addsbdaylem  28063  mulsproplem12  28167  mulsproplem13  28168  mulsproplem14  28169  mulsasslem3  28205  precsexlem11  28255  nnssno  28341  axtgcgrrflx  28484  axtgcgrid  28485  axtgsegcon  28486  axtg5seg  28487  axtgbtwnid  28488  axtgpasch  28489  axtgcont1  28490  tgcgr4  28553  motcgrg  28566  tglng  28568  upgrss  29119  pthdivtx  29761  disjxwwlkn  29942  ex-fpar  30490  nmlno0lem  30821  hlimcaui  31264  chsspwh  31275  shsss  31341  chintcli  31359  shsleji  31398  shub1i  31402  shsval2i  31415  lejdii  31566  spanuni  31572  sshhococi  31574  spansnpji  31606  osumcori  31671  5oai  31689  3oalem6  31695  3oai  31696  pjssmii  31709  mayete3i  31756  mayetes3i  31757  nmlnop0iALT  32023  imaelshi  32086  pjnmopi  32176  pjclem1  32223  pjci  32228  mdslmd1lem1  32353  shatomistici  32389  hatomistici  32390  chpssati  32391  xppreima  32661  iundisjfi  32803  iundisj2fi  32804  fprodex01  32831  xrsmulgzz  32993  fsumrp0cl  33008  gsummpt2co  33033  cycpmfv2  33116  cycpmrn  33145  rlocbas  33253  rlocaddval  33254  rlocmulval  33255  1fldgenq  33303  xrge0slmod  33355  lsmsnorb  33398  idlsrgbas  33511  idlsrgplusg  33512  idlsrgmulr  33514  idlsrgtset  33515  ordtconnlem1  33884  xrge0iifhom  33897  lmlimxrge0  33908  lmxrge0  33912  indsumin  34002  esumcst  34043  esumpfinvallem  34054  esumpfinval  34055  esumpfinvalf  34056  esumcvg  34066  imambfm  34243  elmbfmvol2  34248  sxbrsigalem3  34253  sxbrsigalem2  34267  sxbrsigalem4  34268  sitgclg  34323  eulerpartlem1  34348  eulerpartlemgvv  34357  eulerpartlemgh  34359  eulerpartlemgf  34360  ballotlemfc0  34473  ballotlemfcc  34474  ballotlemiex  34482  ballotlemsup  34485  ballotlemsima  34496  ballotlemrv2  34502  ballotth  34518  signsplypnf  34543  signsply0  34544  rpsqrtcn  34586  itgexpif  34599  fsum2dsub  34600  reprfi2  34616  chtvalz  34622  breprexplemc  34625  breprexpnat  34627  circlemeth  34633  circlemethnat  34634  circlevma  34635  circlemethhgt  34636  hgt750lemd  34641  hgt750lema  34650  tgoldbachgtde  34653  tgoldbachgtda  34654  tgoldbachgt  34656  bnj1145  34985  bnj1286  35011  subfacp1lem2a  35164  erdszelem4  35178  erdszelem5  35179  erdszelem7  35181  erdszelem8  35182  kur14lem7  35196  kur14lem9  35198  resconn  35230  iccllysconn  35234  txpss3v  35859  txprel  35860  limitssson  35892  finminlem  36300  tailf  36357  filnetlem3  36362  onint1  36431  bj-unrab  36908  bj-2upln1upl  37006  bj-imdirco  37172  bj-rvecssabl  37288  taupilem2  37304  taupi  37305  poimirlem3  37609  poimirlem30  37636  poimirlem31  37637  poimirlem32  37638  broucube  37640  opnmbllem0  37642  mblfinlem1  37643  mblfinlem2  37644  mblfinlem3  37645  mblfinlem4  37646  ismblfin  37647  mbfposadd  37653  cnambfre  37654  itg2addnc  37660  ftc1cnnclem  37677  ftc1cnnc  37678  ftc1anclem3  37681  ftc1anclem7  37685  ftc1anc  37687  ftc2nc  37688  dvreasin  37692  dvreacos  37693  areacirclem1  37694  areacirclem2  37695  areacirc  37699  caures  37746  reheibor  37825  xrnss3v  38353  xrnrel  38354  atlatmstc  39300  atlatle  39301  pmaple  39743  sspadd1  39797  sspadd2  39798  dvrelog2  42045  dvrelog3  42046  rpsscn  42311  sumcubes  42325  redvmptabs  42368  diophin  42759  4rexfrabdioph  42785  6rexfrabdioph  42786  irrapxlem1  42809  irrapx1  42815  rmxyelqirr  42897  monotuz  42929  jm2.27dlem5  43001  hbtlem2  43112  algbase  43162  algaddg  43163  algmulr  43164  algsca  43165  algvsca  43166  arearect  43203  areaquad  43204  rtrclex  43606  trclubgNEW  43607  trclexi  43609  rtrclexi  43610  cnvtrcl0  43615  dfrtrcl5  43618  trrelsuperrel2dg  43660  relexpaddss  43707  brtrclfv2  43716  frege131d  43753  xphe  43770  clsk3nimkb  44029  gneispace  44123  k0004val0  44143  inaex  44292  lhe4.4ex1a  44324  uzmptshftfval  44341  binomcxplemdvbinom  44348  binomcxplemcvg  44349  binomcxplemnotnn0  44351  relopabVD  44898  dmwf  44939  rnwf  44940  fzisoeu  45250  fzsscn  45261  fzssre  45264  fzossuz  45330  zssxr  45346  uzssre2  45356  supminfxr  45413  uzsscn  45425  rpssxr  45430  uzinico  45512  limcresiooub  45597  limcresioolb  45598  limcleqr  45599  limclner  45606  limclr  45610  limsupequzmpt2  45673  liminfval2  45723  liminfequzmpt2  45746  icccncfext  45842  cncficcgt0  45843  ioodvbdlimc1lem2  45887  ioodvbdlimc2lem  45889  dvnprodlem2  45902  itgsin0pilem1  45905  itgsinexplem1  45909  itgsinexp  45910  dirkercncflem2  46059  fourierdlem16  46078  fourierdlem18  46080  fourierdlem20  46082  fourierdlem21  46083  fourierdlem22  46084  fourierdlem25  46087  fourierdlem37  46099  fourierdlem42  46104  fourierdlem50  46111  fourierdlem52  46113  fourierdlem62  46123  fourierdlem64  46125  fourierdlem66  46127  fourierdlem68  46129  fourierdlem74  46135  fourierdlem75  46136  fourierdlem76  46137  fourierdlem79  46140  fourierdlem83  46144  fourierdlem95  46156  fourierdlem101  46162  fourierdlem102  46163  fourierdlem103  46164  fourierdlem104  46165  fourierdlem112  46173  fourierdlem114  46175  sqwvfoura  46183  sqwvfourb  46184  fouriersw  46186  etransclem24  46213  etransclem48  46237  sge0sn  46334  sge0tsms  46335  sge0f1o  46337  sge0pr  46349  sge0resplit  46361  sge0split  46364  sge0iunmptlemre  46370  sge0isummpt2  46387  carageniuncllem1  46476  hoicvr  46503  hoicvrrex  46511  hoidmvlelem2  46551  hspmbl  46584  smfmullem4  46749  prmdvdsfmtnof1lem1  47508  prmdvdsfmtnof  47510  oddibas  48016  2zrngbas  48085  2zrng0  48087  sepfsepc  48723  aacllem  49031  amgmlemALT  49033