Theorem sstri 3959

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

Syntax hints:   ⊆ wss 3917

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 3934

This theorem is referenced by:  snsstp1  4783  snsstp2  4784  uniintsn  4952  elopabran  5525  ssrnres  6154  cossxp  6248  foimacnv  6820  ssimaex  6949  riotassuni  7387  oprabss  7500  dmexg  7880  rnexg  7881  fabexgOLD  7918  mptmpoopabbrd  8062  fparlem3  8096  fparlem4  8097  snopsuppss  8161  tposssxp  8212  naddunif  8660  naddasslem1  8661  naddasslem2  8662  mapsspw  8854  sbthlem5  9061  sbthlem7  9063  cnvimamptfin  9311  marypha1lem  9391  ordtypelem4  9481  hartogslem1  9502  ttrclco  9678  cottrcl  9679  tc2  9702  frmin  9709  frrlem16  9718  tz9.12lem1  9747  rankval4  9827  rankxpl  9835  rankmapu  9838  rankxplim  9839  djuin  9878  infxpenlem  9973  ackbij1lem18  10196  cflm  10210  fin23lem29  10301  hsmexlem4  10389  hsmexlem5  10390  brdom3  10488  brdom5  10489  brdom4  10490  smobeth  10546  pwfseqlem3  10620  wundm  10688  wunrn  10689  wunex2  10698  ltsopi  10848  dmaddpi  10850  dmmulpi  10851  nqerf  10890  ltrelxr  11242  uzssre  12822  uzwo2  12878  infssuzle  12897  infssuzcl  12898  uzwo3  12909  nn0ssq  12923  nnssq  12924  qsscn  12926  rpnnen1lem3  12945  rpnnen1lem5  12947  dflt2  13115  ioosscn  13376  unitsscn  13468  fzval2  13478  fzossz  13647  fzossnn  13679  injresinj  13756  flval3  13784  uzsup  13832  uzrdgfni  13930  expcl2lem  14045  rpexpcl  14052  expge0  14070  expge1  14071  hashxrcl  14329  seqcoll  14436  xptrrel  14953  trclublem  14968  01sqrexlem3  15217  limsupval2  15453  limsupgre  15454  rlimpm  15473  rlimclim  15519  isercolllem1  15638  isercolllem2  15639  isercoll  15641  caurcvg  15650  caucvg  15652  summolem2a  15688  summolem2  15689  zsum  15691  fsumcvg3  15702  fsumrpcl  15710  fsumge0  15768  climfsum  15793  ackbijnn  15801  prodmolem2a  15907  prodmolem2  15908  zprod  15910  fprodrpcl  15929  fprodge0  15966  fprodge1  15968  rprisefaccl  15996  divalglem8  16377  sadaddlem  16443  lcmfval  16598  isprm3  16660  maxprmfct  16686  pclem  16816  prmreclem1  16894  prmreclem2  16895  prmreclem3  16896  1arith  16905  4sqlem11  16933  ramtlecl  16978  ramcl2lem  16987  ramxrcl  16995  prmgaplem3  17031  prmgaplem4  17032  cshwshashlem1  17073  structfn  17133  strleun  17134  ressbasss  17216  ressbasss2  17218  srngbase  17280  srngplusg  17281  srngmulr  17282  lmodbase  17296  lmodplusg  17297  lmodsca  17298  ipsbase  17307  ipsaddg  17308  ipsmulr  17309  ipssca  17310  ipsvsca  17311  ipsip  17312  phlbase  17317  phlplusg  17318  phlsca  17319  phlvsca  17320  phlip  17321  odrngbas  17374  odrngplusg  17375  odrngmulr  17376  odrngtset  17377  odrngle  17378  odrngds  17379  prdsvallem  17424  prdsval  17425  prdssca  17426  prdsbas  17427  prdsplusg  17428  prdsmulr  17429  prdsvsca  17430  prdsip  17431  prdsle  17432  prdsds  17434  prdstset  17436  prdshom  17437  prdsco  17438  imasbas  17482  imasds  17483  imasplusg  17487  imasmulr  17488  imassca  17489  imasvsca  17490  imasip  17491  imastset  17492  imasle  17493  wunfunc  17870  fullfunc  17877  fthfunc  17878  isfull  17881  isfth  17885  wunnat  17928  dmcoass  18035  catcisolem  18079  catciso  18080  catcoppccl  18086  catcfuccl  18087  catcxpccl  18175  ipobas  18497  ipolerval  18498  ipotset  18499  psdmrn  18539  psss  18546  ledm  18556  lern  18557  dirdm  18566  dirge  18569  mulgfval  19008  mvdco  19382  f1omvdconj  19383  gexex  19790  gsumval3  19844  lssacs  20880  cnfldbas  21275  mpocnfldadd  21276  mpocnfldmul  21278  cnfldcj  21280  cnfldtset  21281  cnfldle  21282  cnfldds  21283  cnfldunif  21284  cnfldbasOLD  21290  cnfldaddOLD  21291  cnfldmulOLD  21292  cnfldcjOLD  21293  cnfldtsetOLD  21294  cnfldleOLD  21295  cnflddsOLD  21296  cnfldunifOLD  21297  rge0srg  21362  zntoslem  21473  asplss  21790  aspsubrg  21792  psrass1lem  21848  psrbas  21849  psrplusg  21852  psrmulr  21858  psrsca  21863  psrvscafval  21864  psrass1  21880  psrass23l  21883  psrcom  21884  psrass23  21885  psropprmul  22129  coe1mul2  22162  ofco2  22345  toponsspwpw  22816  dmtopon  22817  leordtval2  23106  lmbrf  23154  lmres  23194  fiuncmp  23298  comppfsc  23426  1stckgenlem  23447  kgencn3  23452  ptbasfi  23475  xkoopn  23483  txcnmpt  23518  txkgen  23546  opnfbas  23736  fmfnfmlem4  23851  tsmsxplem1  24047  trust  24124  restutop  24132  nmoffn  24606  nmofval  24609  nmogelb  24611  nmolb  24612  nmof  24614  qtopbas  24654  tgqioo  24695  re2ndc  24696  iitopon  24779  dfii3  24783  iimulcnOLD  24842  cnheiborlem  24860  bndth  24864  lebnumii  24872  reparphtiOLD  24904  pcoass  24931  cphsqrtcl  25091  lmmbrf  25169  iscauf  25187  caucfil  25190  lmclimf  25211  rrxmval  25312  rrxmet  25315  ovolfioo  25375  ovolficc  25376  ovolficcss  25377  ovolfsf  25379  ovollb  25387  ovolicc2lem3  25427  ovolicc2lem4  25428  ovolicc2  25430  volf  25437  volsup  25464  ovolfs2  25479  uniiccdif  25486  uniioovol  25487  uniiccvol  25488  uniioombllem2  25491  uniioombllem3a  25492  uniioombllem3  25493  uniioombllem4  25494  uniioombllem5  25495  uniioombl  25497  dyadmbllem  25507  dyadmbl  25508  opnmbllem  25509  opnmblALT  25511  volsup2  25513  vitalilem4  25519  vitalilem5  25520  vitali  25521  mbfimaopnlem  25563  mbflimsup  25574  i1f0  25595  i1f1  25598  itg11  25599  itg2mulc  25655  itg2gt0  25668  ellimc2  25785  limcresi  25793  dvreslem  25817  dvres2lem  25818  dvaddbr  25847  dvmulbr  25848  dvmulbrOLD  25849  dvlipcn  25906  c1liplem1  25908  lhop1lem  25925  lhop1  25926  lhop2  25927  lhop  25928  dvfsumrlim  25945  ftc1cn  25957  itgsubstlem  25962  itgsubst  25963  itgpowd  25964  mdegleb  25976  mdeglt  25977  mdegldg  25978  mdegxrcl  25979  mdegcl  25981  mdegaddle  25986  mdegmullem  25990  deg1mul3le  26029  ig1peu  26087  ig1pdvds  26092  aacjcl  26242  aannenlem2  26244  aannenlem3  26245  aalioulem2  26248  taylfval  26273  radcnvcl  26333  radcnvlt1  26334  radcnvle  26336  abelth  26358  abelth2  26359  pilem2  26369  pilem3  26370  pige3ALT  26436  recosf1o  26451  resinf1o  26452  tanord1  26453  logcn  26563  dvlog  26567  dvlog2lem  26568  efopn  26574  logtayl  26576  cxpcn3  26665  loglesqrt  26678  ssscongptld  26739  leibpi  26859  efrlim  26886  efrlimOLD  26887  jensenlem1  26904  jensenlem2  26905  jensen  26906  amgm  26908  lgamgulmlem2  26947  ftalem5  26994  efnnfsumcl  27020  efchtdvds  27076  mpodvdsmulf1o  27111  fsumdvdsmul  27112  dvdsmulf1o  27113  fsumdvdsmulOLD  27114  lgsfcl2  27221  2sqlem6  27341  2sqlem8  27344  2sqlem9  27345  rpvmasumlem  27405  rpvmasum2  27430  dchrisum0re  27431  dchrisum0lem3  27437  dchrisum0  27438  rplogsum  27445  dirith2  27446  noextendseq  27586  oldf  27772  leftssno  27799  rightssno  27800  addsbdaylem  27930  mulsproplem12  28037  mulsproplem13  28038  mulsproplem14  28039  mulsasslem3  28075  precsexlem11  28126  onscutlt  28172  bdayon  28180  nnssno  28222  axtgcgrrflx  28396  axtgcgrid  28397  axtgsegcon  28398  axtg5seg  28399  axtgbtwnid  28400  axtgpasch  28401  axtgcont1  28402  tgcgr4  28465  motcgrg  28478  tglng  28480  upgrss  29022  pthdivtx  29664  disjxwwlkn  29850  ex-fpar  30398  nmlno0lem  30729  hlimcaui  31172  chsspwh  31183  shsss  31249  chintcli  31267  shsleji  31306  shub1i  31310  shsval2i  31323  lejdii  31474  spanuni  31480  sshhococi  31482  spansnpji  31514  osumcori  31579  5oai  31597  3oalem6  31603  3oai  31604  pjssmii  31617  mayete3i  31664  mayetes3i  31665  nmlnop0iALT  31931  imaelshi  31994  pjnmopi  32084  pjclem1  32131  pjci  32136  mdslmd1lem1  32261  shatomistici  32297  hatomistici  32298  chpssati  32299  xppreima  32576  iundisjfi  32726  iundisj2fi  32727  fprodex01  32757  indsumin  32792  xrsmulgzz  32954  fsumrp0cl  32969  gsummpt2co  32995  cycpmfv2  33078  cycpmrn  33107  rlocbas  33225  rlocaddval  33226  rlocmulval  33227  1fldgenq  33279  xrge0slmod  33326  lsmsnorb  33369  idlsrgbas  33482  idlsrgplusg  33483  idlsrgmulr  33485  idlsrgtset  33486  constrextdg2  33746  ordtconnlem1  33921  xrge0iifhom  33934  lmlimxrge0  33945  lmxrge0  33949  esumcst  34060  esumpfinvallem  34071  esumpfinval  34072  esumpfinvalf  34073  esumcvg  34083  imambfm  34260  elmbfmvol2  34265  sxbrsigalem3  34270  sxbrsigalem2  34284  sxbrsigalem4  34285  sitgclg  34340  eulerpartlem1  34365  eulerpartlemgvv  34374  eulerpartlemgh  34376  eulerpartlemgf  34377  ballotlemfc0  34491  ballotlemfcc  34492  ballotlemiex  34500  ballotlemsup  34503  ballotlemsima  34514  ballotlemrv2  34520  ballotth  34536  signsplypnf  34548  signsply0  34549  rpsqrtcn  34591  itgexpif  34604  fsum2dsub  34605  reprfi2  34621  chtvalz  34627  breprexplemc  34630  breprexpnat  34632  circlemeth  34638  circlemethnat  34639  circlevma  34640  circlemethhgt  34641  hgt750lemd  34646  hgt750lema  34655  tgoldbachgtde  34658  tgoldbachgtda  34659  tgoldbachgt  34661  bnj1145  34990  bnj1286  35016  subfacp1lem2a  35174  erdszelem4  35188  erdszelem5  35189  erdszelem7  35191  erdszelem8  35192  kur14lem7  35206  kur14lem9  35208  resconn  35240  iccllysconn  35244  txpss3v  35873  txprel  35874  limitssson  35906  finminlem  36313  tailf  36370  filnetlem3  36375  onint1  36444  bj-unrab  36921  bj-2upln1upl  37019  bj-imdirco  37185  bj-rvecssabl  37301  taupilem2  37317  taupi  37318  poimirlem3  37624  poimirlem30  37651  poimirlem31  37652  poimirlem32  37653  broucube  37655  opnmbllem0  37657  mblfinlem1  37658  mblfinlem2  37659  mblfinlem3  37660  mblfinlem4  37661  ismblfin  37662  mbfposadd  37668  cnambfre  37669  itg2addnc  37675  ftc1cnnclem  37692  ftc1cnnc  37693  ftc1anclem3  37696  ftc1anclem7  37700  ftc1anc  37702  ftc2nc  37703  dvreasin  37707  dvreacos  37708  areacirclem1  37709  areacirclem2  37710  areacirc  37714  caures  37761  reheibor  37840  xrnss3v  38361  xrnrel  38362  atlatmstc  39319  atlatle  39320  pmaple  39762  sspadd1  39816  sspadd2  39817  dvrelog2  42059  dvrelog3  42060  rpsscn  42294  sumcubes  42308  redvmptabs  42355  diophin  42767  4rexfrabdioph  42793  6rexfrabdioph  42794  irrapxlem1  42817  irrapx1  42823  rmxyelqirr  42905  monotuz  42937  jm2.27dlem5  43009  hbtlem2  43120  algbase  43170  algaddg  43171  algmulr  43172  algsca  43173  algvsca  43174  arearect  43211  areaquad  43212  rtrclex  43613  trclubgNEW  43614  trclexi  43616  rtrclexi  43617  cnvtrcl0  43622  dfrtrcl5  43625  trrelsuperrel2dg  43667  relexpaddss  43714  brtrclfv2  43723  frege131d  43760  xphe  43777  clsk3nimkb  44036  gneispace  44130  k0004val0  44150  inaex  44293  lhe4.4ex1a  44325  uzmptshftfval  44342  binomcxplemdvbinom  44349  binomcxplemcvg  44350  binomcxplemnotnn0  44352  relopabVD  44897  dmwf  44962  rnwf  44963  fzisoeu  45305  fzsscn  45316  fzssre  45319  fzossuz  45384  zssxr  45400  uzssre2  45410  supminfxr  45467  uzsscn  45478  rpssxr  45483  uzinico  45564  limcresiooub  45647  limcresioolb  45648  limcleqr  45649  limclner  45656  limclr  45660  limsupequzmpt2  45723  liminfval2  45773  liminfequzmpt2  45796  icccncfext  45892  cncficcgt0  45893  ioodvbdlimc1lem2  45937  ioodvbdlimc2lem  45939  dvnprodlem2  45952  itgsin0pilem1  45955  itgsinexplem1  45959  itgsinexp  45960  dirkercncflem2  46109  fourierdlem16  46128  fourierdlem18  46130  fourierdlem20  46132  fourierdlem21  46133  fourierdlem22  46134  fourierdlem25  46137  fourierdlem37  46149  fourierdlem42  46154  fourierdlem50  46161  fourierdlem52  46163  fourierdlem62  46173  fourierdlem64  46175  fourierdlem66  46177  fourierdlem68  46179  fourierdlem74  46185  fourierdlem75  46186  fourierdlem76  46187  fourierdlem79  46190  fourierdlem83  46194  fourierdlem95  46206  fourierdlem101  46212  fourierdlem102  46213  fourierdlem103  46214  fourierdlem104  46215  fourierdlem112  46223  fourierdlem114  46225  sqwvfoura  46233  sqwvfourb  46234  fouriersw  46236  etransclem24  46263  etransclem48  46287  sge0sn  46384  sge0tsms  46385  sge0f1o  46387  sge0pr  46399  sge0resplit  46411  sge0split  46414  sge0iunmptlemre  46420  sge0isummpt2  46437  carageniuncllem1  46526  hoicvr  46553  hoicvrrex  46561  hoidmvlelem2  46601  hspmbl  46634  smfmullem4  46799  lamberte  46896  rehalfge1  47340  prmdvdsfmtnof1lem1  47589  prmdvdsfmtnof  47591  upgrimpthslem2  47912  upgrimpths  47913  oddibas  48165  2zrngbas  48234  2zrng0  48236  dmtposss  48868  tposres3  48873  sepfsepc  48920  uptrlem1  49203  uptrlem2  49204  uptrlem3  49205  uptra  49208  uptrar  49209  uobeqw  49212  uptr2  49214  uptr2a  49215  fucoppcfunc  49405  aacllem  49794  amgmlemALT  49796