Theorem sstri 3992

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

Syntax hints:   ⊆ wss 3949

This theorem was proved from axioms:  ax-mp 5  ax-1 6  ax-2 7  ax-3 8  ax-gen 1798  ax-4 1812  ax-5 1914  ax-6 1972  ax-7 2012  ax-8 2109  ax-9 2117  ax-ext 2704

This theorem depends on definitions:  df-bi 206  df-an 398  df-tru 1545  df-ex 1783  df-sb 2069  df-clab 2711  df-cleq 2725  df-clel 2811  df-v 3477  df-in 3956  df-ss 3966

This theorem is referenced by:  snsstp1  4820  snsstp2  4821  uniintsn  4992  elopabran  5563  ssrnres  6178  cossxp  6272  foimacnv  6851  ssimaex  6977  riotassuni  7406  oprabss  7515  dmexg  7894  rnexg  7895  fabexg  7925  fparlem3  8100  fparlem4  8101  snopsuppss  8164  tposssxp  8215  naddunif  8692  naddasslem1  8693  naddasslem2  8694  mapsspw  8872  sbthlem5  9087  sbthlem7  9089  cnvimamptfin  9353  marypha1lem  9428  ordtypelem4  9516  hartogslem1  9537  ttrclco  9713  cottrcl  9714  tc2  9737  frmin  9744  frrlem16  9753  tz9.12lem1  9782  rankval4  9862  rankxpl  9870  rankmapu  9873  rankxplim  9874  djuin  9913  infxpenlem  10008  ackbij1lem18  10232  cflm  10245  fin23lem29  10336  hsmexlem4  10424  hsmexlem5  10425  brdom3  10523  brdom5  10524  brdom4  10525  smobeth  10581  pwfseqlem3  10655  wundm  10723  wunrn  10724  wunex2  10733  ltsopi  10883  dmaddpi  10885  dmmulpi  10886  nqerf  10925  ltrelxr  11275  uzssre  12844  uzwo2  12896  infssuzle  12915  infssuzcl  12916  uzwo3  12927  nn0ssq  12941  nnssq  12942  qsscn  12944  rpnnen1lem3  12963  rpnnen1lem5  12965  dflt2  13127  ioosscn  13386  unitsscn  13477  fzval2  13487  fzossz  13652  fzossnn  13681  injresinj  13753  flval3  13780  uzsup  13828  uzrdgfni  13923  expcl2lem  14039  rpexpcl  14046  expge0  14064  expge1  14065  hashxrcl  14317  seqcoll  14425  xptrrel  14927  trclublem  14942  01sqrexlem3  15191  limsupval2  15424  limsupgre  15425  rlimpm  15444  rlimclim  15490  isercolllem1  15611  isercolllem2  15612  isercoll  15614  caurcvg  15623  caucvg  15625  summolem2a  15661  summolem2  15662  zsum  15664  fsumcvg3  15675  fsumrpcl  15683  fsumge0  15741  climfsum  15766  ackbijnn  15774  prodmolem2a  15878  prodmolem2  15879  zprod  15881  fprodrpcl  15900  fprodge0  15937  fprodge1  15939  rprisefaccl  15967  divalglem8  16343  sadaddlem  16407  lcmfval  16558  isprm3  16620  maxprmfct  16646  pclem  16771  prmreclem1  16849  prmreclem2  16850  prmreclem3  16851  1arith  16860  4sqlem11  16888  ramtlecl  16933  ramcl2lem  16942  ramxrcl  16950  prmgaplem3  16986  prmgaplem4  16987  cshwshashlem1  17029  structfn  17089  strleun  17090  ressbasss  17183  ressbasss2  17185  srngbase  17255  srngplusg  17256  srngmulr  17257  lmodbase  17271  lmodplusg  17272  lmodsca  17273  ipsbase  17282  ipsaddg  17283  ipsmulr  17284  ipssca  17285  ipsvsca  17286  ipsip  17287  phlbase  17292  phlplusg  17293  phlsca  17294  phlvsca  17295  phlip  17296  odrngbas  17349  odrngplusg  17350  odrngmulr  17351  odrngtset  17352  odrngle  17353  odrngds  17354  prdsvallem  17400  prdsval  17401  prdssca  17402  prdsbas  17403  prdsplusg  17404  prdsmulr  17405  prdsvsca  17406  prdsip  17407  prdsle  17408  prdsds  17410  prdstset  17412  prdshom  17413  prdsco  17414  imasbas  17458  imasds  17459  imasplusg  17463  imasmulr  17464  imassca  17465  imasvsca  17466  imasip  17467  imastset  17468  imasle  17469  wunfunc  17849  wunfuncOLD  17850  fullfunc  17857  fthfunc  17858  isfull  17861  isfth  17865  wunnat  17907  wunnatOLD  17908  dmcoass  18016  catcisolem  18060  catciso  18061  catcoppccl  18067  catcoppcclOLD  18068  catcfuccl  18069  catcfucclOLD  18070  catcxpccl  18159  catcxpcclOLD  18160  ipobas  18484  ipolerval  18485  ipotset  18486  psdmrn  18526  psss  18533  ledm  18543  lern  18544  dirdm  18553  dirge  18556  mulgfval  18952  mvdco  19313  f1omvdconj  19314  gexex  19721  gsumval3  19775  lssacs  20578  cnfldbas  20948  cnfldadd  20949  cnfldmul  20950  cnfldcj  20951  cnfldtset  20952  cnfldle  20953  cnfldds  20954  cnfldunif  20955  rge0srg  21016  zntoslem  21112  asplss  21428  aspsubrg  21430  psrass1lemOLD  21493  psrass1lem  21496  psrbas  21497  psrplusg  21500  psrmulr  21503  psrsca  21508  psrvscafval  21509  psrass1  21525  psrass23l  21528  psrcom  21529  psrass23  21530  psropprmul  21760  coe1mul2  21791  ofco2  21953  toponsspwpw  22424  dmtopon  22425  leordtval2  22716  lmbrf  22764  lmres  22804  fiuncmp  22908  comppfsc  23036  1stckgenlem  23057  kgencn3  23062  ptbasfi  23085  xkoopn  23093  txcnmpt  23128  txkgen  23156  opnfbas  23346  fmfnfmlem4  23461  tsmsxplem1  23657  trust  23734  restutop  23742  nmoffn  24228  nmofval  24231  nmogelb  24233  nmolb  24234  nmof  24236  qtopbas  24276  tgqioo  24316  re2ndc  24317  iitopon  24395  dfii3  24399  iimulcn  24454  cnheiborlem  24470  bndth  24474  lebnumii  24482  reparphti  24513  pcoass  24540  cphsqrtcl  24701  lmmbrf  24779  iscauf  24797  caucfil  24800  lmclimf  24821  rrxmval  24922  rrxmet  24925  ovolfioo  24984  ovolficc  24985  ovolficcss  24986  ovolfsf  24988  ovollb  24996  ovolicc2lem3  25036  ovolicc2lem4  25037  ovolicc2  25039  volf  25046  volsup  25073  ovolfs2  25088  uniiccdif  25095  uniioovol  25096  uniiccvol  25097  uniioombllem2  25100  uniioombllem3a  25101  uniioombllem3  25102  uniioombllem4  25103  uniioombllem5  25104  uniioombl  25106  dyadmbllem  25116  dyadmbl  25117  opnmbllem  25118  opnmblALT  25120  volsup2  25122  vitalilem4  25128  vitalilem5  25129  vitali  25130  mbfimaopnlem  25172  mbflimsup  25183  i1f0  25204  i1f1  25207  itg11  25208  itg2mulc  25265  itg2gt0  25278  ellimc2  25394  limcresi  25402  dvreslem  25426  dvres2lem  25427  dvaddbr  25455  dvmulbr  25456  dvlipcn  25511  c1liplem1  25513  lhop1lem  25530  lhop1  25531  lhop2  25532  lhop  25533  dvfsumrlim  25548  ftc1cn  25560  itgsubstlem  25565  itgsubst  25566  itgpowd  25567  mdegleb  25582  mdeglt  25583  mdegldg  25584  mdegxrcl  25585  mdegcl  25587  mdegaddle  25592  mdegmullem  25596  deg1mul3le  25634  ig1peu  25689  ig1pdvds  25694  aacjcl  25840  aannenlem2  25842  aannenlem3  25843  aalioulem2  25846  taylfval  25871  radcnvcl  25929  radcnvlt1  25930  radcnvle  25932  abelth  25953  abelth2  25954  pilem2  25964  pilem3  25965  pige3ALT  26029  recosf1o  26044  resinf1o  26045  tanord1  26046  logcn  26155  dvlog  26159  dvlog2lem  26160  efopn  26166  logtayl  26168  cxpcn3  26256  loglesqrt  26266  ssscongptld  26327  leibpi  26447  efrlim  26474  jensenlem1  26491  jensenlem2  26492  jensen  26493  amgm  26495  lgamgulmlem2  26534  ftalem5  26581  efnnfsumcl  26607  efchtdvds  26663  dvdsmulf1o  26698  fsumdvdsmul  26699  lgsfcl2  26806  2sqlem6  26926  2sqlem8  26929  2sqlem9  26930  rpvmasumlem  26990  rpvmasum2  27015  dchrisum0re  27016  dchrisum0lem3  27022  dchrisum0  27023  rplogsum  27030  dirith2  27031  noextendseq  27170  oldf  27352  leftssno  27375  rightssno  27376  mulsproplem12  27583  mulsproplem13  27584  mulsproplem14  27585  mulsasslem3  27620  precsexlem11  27663  axtgcgrrflx  27713  axtgcgrid  27714  axtgsegcon  27715  axtg5seg  27716  axtgbtwnid  27717  axtgpasch  27718  axtgcont1  27719  tgcgr4  27782  motcgrg  27795  tglng  27797  upgrss  28348  pthdivtx  28986  disjxwwlkn  29167  ex-fpar  29715  nmlno0lem  30046  hlimcaui  30489  chsspwh  30500  shsss  30566  chintcli  30584  shsleji  30623  shub1i  30627  shsval2i  30640  lejdii  30791  spanuni  30797  sshhococi  30799  spansnpji  30831  osumcori  30896  5oai  30914  3oalem6  30920  3oai  30921  pjssmii  30934  mayete3i  30981  mayetes3i  30982  nmlnop0iALT  31248  imaelshi  31311  pjnmopi  31401  pjclem1  31448  pjci  31453  mdslmd1lem1  31578  shatomistici  31614  hatomistici  31615  chpssati  31616  xppreima  31871  iundisjfi  32007  iundisj2fi  32008  fprodex01  32031  xrsmulgzz  32179  fsumrp0cl  32196  gsummpt2co  32200  cycpmfv2  32273  cycpmrn  32302  1fldgenq  32412  xrge0slmod  32463  lsmsnorb  32501  idlsrgbas  32618  idlsrgplusg  32619  idlsrgmulr  32621  idlsrgtset  32622  ordtconnlem1  32904  xrge0iifhom  32917  lmlimxrge0  32928  lmxrge0  32932  indsumin  33020  esumcst  33061  esumpfinvallem  33072  esumpfinval  33073  esumpfinvalf  33074  esumcvg  33084  imambfm  33261  elmbfmvol2  33266  sxbrsigalem3  33271  sxbrsigalem2  33285  sxbrsigalem4  33286  sitgclg  33341  eulerpartlem1  33366  eulerpartlemgvv  33375  eulerpartlemgh  33377  eulerpartlemgf  33378  ballotlemfc0  33491  ballotlemfcc  33492  ballotlemiex  33500  ballotlemsup  33503  ballotlemsima  33514  ballotlemrv2  33520  ballotth  33536  signsplypnf  33561  signsply0  33562  rpsqrtcn  33605  itgexpif  33618  fsum2dsub  33619  reprfi2  33635  chtvalz  33641  breprexplemc  33644  breprexpnat  33646  circlemeth  33652  circlemethnat  33653  circlevma  33654  circlemethhgt  33655  hgt750lemd  33660  hgt750lema  33669  tgoldbachgtde  33672  tgoldbachgtda  33673  tgoldbachgt  33675  bnj1145  34004  bnj1286  34030  subfacp1lem2a  34171  erdszelem4  34185  erdszelem5  34186  erdszelem7  34188  erdszelem8  34189  kur14lem7  34203  kur14lem9  34205  cvxpconn  34233  cvxsconn  34234  resconn  34237  iccllysconn  34241  txpss3v  34850  txprel  34851  limitssson  34883  gg-dvmulbr  35175  finminlem  35203  tailf  35260  filnetlem3  35265  onint1  35334  bj-unrab  35806  bj-2upln1upl  35905  bj-imdirco  36071  bj-rvecssabl  36187  taupilem2  36203  taupi  36204  poimirlem3  36491  poimirlem30  36518  poimirlem31  36519  poimirlem32  36520  broucube  36522  opnmbllem0  36524  mblfinlem1  36525  mblfinlem2  36526  mblfinlem3  36527  mblfinlem4  36528  ismblfin  36529  mbfposadd  36535  cnambfre  36536  itg2addnc  36542  ftc1cnnclem  36559  ftc1cnnc  36560  ftc1anclem3  36563  ftc1anclem7  36567  ftc1anc  36569  ftc2nc  36570  dvreasin  36574  dvreacos  36575  areacirclem1  36576  areacirclem2  36577  areacirc  36581  caures  36628  reheibor  36707  xrnss3v  37242  xrnrel  37243  atlatmstc  38189  atlatle  38190  pmaple  38632  sspadd1  38686  sspadd2  38687  dvrelog2  40929  dvrelog3  40930  sumcubes  41211  diophin  41510  4rexfrabdioph  41536  6rexfrabdioph  41537  irrapxlem1  41560  irrapx1  41566  rmxyelqirr  41648  monotuz  41680  jm2.27dlem5  41752  hbtlem2  41866  algbase  41920  algaddg  41921  algmulr  41922  algsca  41923  algvsca  41924  arearect  41964  areaquad  41965  rtrclex  42368  trclubgNEW  42369  trclexi  42371  rtrclexi  42372  cnvtrcl0  42377  dfrtrcl5  42380  trrelsuperrel2dg  42422  relexpaddss  42469  brtrclfv2  42478  frege131d  42515  xphe  42532  clsk3nimkb  42791  gneispace  42885  k0004val0  42905  inaex  43056  lhe4.4ex1a  43088  uzmptshftfval  43105  binomcxplemdvbinom  43112  binomcxplemcvg  43113  binomcxplemnotnn0  43115  relopabVD  43662  fzisoeu  44010  fzsscn  44021  fzssre  44024  fzossuz  44091  zssxr  44107  uzssre2  44117  supminfxr  44174  uzsscn  44186  rpssxr  44191  uzinico  44273  limcresiooub  44358  limcresioolb  44359  limcleqr  44360  limclner  44367  limclr  44371  limsupequzmpt2  44434  liminfval2  44484  liminfequzmpt2  44507  icccncfext  44603  cncficcgt0  44604  ioodvbdlimc1lem2  44648  ioodvbdlimc2lem  44650  dvnprodlem1  44662  dvnprodlem2  44663  itgsin0pilem1  44666  itgsinexplem1  44670  itgsinexp  44671  dirkercncflem2  44820  fourierdlem16  44839  fourierdlem18  44841  fourierdlem20  44843  fourierdlem21  44844  fourierdlem22  44845  fourierdlem25  44848  fourierdlem37  44860  fourierdlem42  44865  fourierdlem50  44872  fourierdlem52  44874  fourierdlem62  44884  fourierdlem64  44886  fourierdlem66  44888  fourierdlem68  44890  fourierdlem74  44896  fourierdlem75  44897  fourierdlem76  44898  fourierdlem79  44901  fourierdlem83  44905  fourierdlem95  44917  fourierdlem101  44923  fourierdlem102  44924  fourierdlem103  44925  fourierdlem104  44926  fourierdlem112  44934  fourierdlem114  44936  sqwvfoura  44944  sqwvfourb  44945  fouriersw  44947  etransclem24  44974  etransclem48  44998  sge0sn  45095  sge0tsms  45096  sge0f1o  45098  sge0pr  45110  sge0resplit  45122  sge0split  45125  sge0iunmptlemre  45131  sge0isummpt2  45148  carageniuncllem1  45237  hoicvr  45264  hoicvrrex  45272  hoidmvlelem2  45312  hspmbl  45345  smfmullem4  45510  prmdvdsfmtnof1lem1  46252  prmdvdsfmtnof  46254  oddibas  46583  2zrngbas  46834  2zrng0  46836  sepfsepc  47560  aacllem  47848  amgmlemALT  47850