Theorem sstri 3951

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

Syntax hints:   ⊆ wss 3908

This theorem was proved from axioms:  ax-mp 5  ax-1 6  ax-2 7  ax-3 8  ax-gen 1797  ax-4 1811  ax-5 1913  ax-6 1971  ax-7 2011  ax-8 2108  ax-9 2116  ax-ext 2707

This theorem depends on definitions:  df-bi 206  df-an 397  df-tru 1544  df-ex 1782  df-sb 2068  df-clab 2714  df-cleq 2728  df-clel 2814  df-v 3445  df-in 3915  df-ss 3925

This theorem is referenced by:  snsstp1  4774  snsstp2  4775  uniintsn  4946  elopabran  5517  ssrnres  6128  cossxp  6222  foimacnv  6798  ssimaex  6923  riotassuni  7350  oprabss  7459  dmexg  7836  rnexg  7837  fabexg  7867  fparlem3  8042  fparlem4  8043  snopsuppss  8106  tposssxp  8157  naddunif  8633  naddasslem1  8634  naddasslem2  8635  mapsspw  8812  sbthlem5  9027  sbthlem7  9029  cnvimamptfin  9293  marypha1lem  9365  ordtypelem4  9453  hartogslem1  9474  ttrclco  9650  cottrcl  9651  tc2  9674  frmin  9681  frrlem16  9690  tz9.12lem1  9719  rankval4  9799  rankxpl  9807  rankmapu  9810  rankxplim  9811  djuin  9850  infxpenlem  9945  ackbij1lem18  10169  cflm  10182  fin23lem29  10273  hsmexlem4  10361  hsmexlem5  10362  brdom3  10460  brdom5  10461  brdom4  10462  smobeth  10518  pwfseqlem3  10592  wundm  10660  wunrn  10661  wunex2  10670  ltsopi  10820  dmaddpi  10822  dmmulpi  10823  nqerf  10862  ltrelxr  11212  uzssre  12781  uzwo2  12829  infssuzle  12848  infssuzcl  12849  uzwo3  12860  nn0ssq  12874  nnssq  12875  qsscn  12877  rpnnen1lem3  12896  rpnnen1lem5  12898  dflt2  13059  ioosscn  13318  unitsscn  13409  fzval2  13419  fzossz  13584  fzossnn  13613  injresinj  13685  flval3  13712  uzsup  13760  uzrdgfni  13855  expcl2lem  13971  rpexpcl  13978  expge0  13996  expge1  13997  hashxrcl  14249  seqcoll  14355  xptrrel  14857  trclublem  14872  01sqrexlem3  15121  limsupval2  15354  limsupgre  15355  rlimpm  15374  rlimclim  15420  isercolllem1  15541  isercolllem2  15542  isercoll  15544  caurcvg  15553  caucvg  15555  summolem2a  15592  summolem2  15593  zsum  15595  fsumcvg3  15606  fsumrpcl  15614  fsumge0  15672  climfsum  15697  ackbijnn  15705  prodmolem2a  15809  prodmolem2  15810  zprod  15812  fprodrpcl  15831  fprodge0  15868  fprodge1  15870  rprisefaccl  15898  divalglem8  16274  sadaddlem  16338  lcmfval  16489  isprm3  16551  maxprmfct  16577  pclem  16702  prmreclem1  16780  prmreclem2  16781  prmreclem3  16782  1arith  16791  4sqlem11  16819  ramtlecl  16864  ramcl2lem  16873  ramxrcl  16881  prmgaplem3  16917  prmgaplem4  16918  cshwshashlem1  16960  structfn  17020  strleun  17021  srngbase  17183  srngplusg  17184  srngmulr  17185  lmodbase  17199  lmodplusg  17200  lmodsca  17201  ipsbase  17210  ipsaddg  17211  ipsmulr  17212  ipssca  17213  ipsvsca  17214  ipsip  17215  phlbase  17220  phlplusg  17221  phlsca  17222  phlvsca  17223  phlip  17224  odrngbas  17277  odrngplusg  17278  odrngmulr  17279  odrngtset  17280  odrngle  17281  odrngds  17282  prdsvallem  17328  prdsval  17329  prdssca  17330  prdsbas  17331  prdsplusg  17332  prdsmulr  17333  prdsvsca  17334  prdsip  17335  prdsle  17336  prdsds  17338  prdstset  17340  prdshom  17341  prdsco  17342  imasbas  17386  imasds  17387  imasplusg  17391  imasmulr  17392  imassca  17393  imasvsca  17394  imasip  17395  imastset  17396  imasle  17397  wunfunc  17777  wunfuncOLD  17778  fullfunc  17785  fthfunc  17786  isfull  17789  isfth  17793  wunnat  17835  wunnatOLD  17836  dmcoass  17944  catcisolem  17988  catciso  17989  catcoppccl  17995  catcoppcclOLD  17996  catcfuccl  17997  catcfucclOLD  17998  catcxpccl  18087  catcxpcclOLD  18088  ipobas  18412  ipolerval  18413  ipotset  18414  psdmrn  18454  psss  18461  ledm  18471  lern  18472  dirdm  18481  dirge  18484  mulgfval  18865  mvdco  19218  f1omvdconj  19219  gexex  19622  gsumval3  19675  lssacs  20413  cnfldbas  20785  cnfldadd  20786  cnfldmul  20787  cnfldcj  20788  cnfldtset  20789  cnfldle  20790  cnfldds  20791  cnfldunif  20792  rge0srg  20853  zntoslem  20948  asplss  21262  aspsubrg  21264  psrass1lemOLD  21327  psrass1lem  21330  psrbas  21331  psrplusg  21334  psrmulr  21337  psrsca  21342  psrvscafval  21343  psrass1  21358  psrass23l  21361  psrcom  21362  psrass23  21363  psropprmul  21593  coe1mul2  21624  ofco2  21784  toponsspwpw  22255  dmtopon  22256  leordtval2  22547  lmbrf  22595  lmres  22635  fiuncmp  22739  comppfsc  22867  1stckgenlem  22888  kgencn3  22893  ptbasfi  22916  xkoopn  22924  txcnmpt  22959  txkgen  22987  opnfbas  23177  fmfnfmlem4  23292  tsmsxplem1  23488  trust  23565  restutop  23573  nmoffn  24059  nmofval  24062  nmogelb  24064  nmolb  24065  nmof  24067  qtopbas  24107  tgqioo  24147  re2ndc  24148  iitopon  24226  dfii3  24230  iimulcn  24285  cnheiborlem  24301  bndth  24305  lebnumii  24313  reparphti  24344  pcoass  24371  cphsqrtcl  24532  lmmbrf  24610  iscauf  24628  caucfil  24631  lmclimf  24652  rrxmval  24753  rrxmet  24756  ovolfioo  24815  ovolficc  24816  ovolficcss  24817  ovolfsf  24819  ovollb  24827  ovolicc2lem3  24867  ovolicc2lem4  24868  ovolicc2  24870  volf  24877  volsup  24904  ovolfs2  24919  uniiccdif  24926  uniioovol  24927  uniiccvol  24928  uniioombllem2  24931  uniioombllem3a  24932  uniioombllem3  24933  uniioombllem4  24934  uniioombllem5  24935  uniioombl  24937  dyadmbllem  24947  dyadmbl  24948  opnmbllem  24949  opnmblALT  24951  volsup2  24953  vitalilem4  24959  vitalilem5  24960  vitali  24961  mbfimaopnlem  25003  mbflimsup  25014  i1f0  25035  i1f1  25038  itg11  25039  itg2mulc  25096  itg2gt0  25109  ellimc2  25225  limcresi  25233  dvreslem  25257  dvres2lem  25258  dvaddbr  25286  dvmulbr  25287  dvlipcn  25342  c1liplem1  25344  lhop1lem  25361  lhop1  25362  lhop2  25363  lhop  25364  dvfsumrlim  25379  ftc1cn  25391  itgsubstlem  25396  itgsubst  25397  itgpowd  25398  mdegleb  25413  mdeglt  25414  mdegldg  25415  mdegxrcl  25416  mdegcl  25418  mdegaddle  25423  mdegmullem  25427  deg1mul3le  25465  ig1peu  25520  ig1pdvds  25525  aacjcl  25671  aannenlem2  25673  aannenlem3  25674  aalioulem2  25677  taylfval  25702  radcnvcl  25760  radcnvlt1  25761  radcnvle  25763  abelth  25784  abelth2  25785  pilem2  25795  pilem3  25796  pige3ALT  25860  recosf1o  25875  resinf1o  25876  tanord1  25877  logcn  25986  dvlog  25990  dvlog2lem  25991  efopn  25997  logtayl  25999  cxpcn3  26085  loglesqrt  26095  ssscongptld  26156  leibpi  26276  efrlim  26303  jensenlem1  26320  jensenlem2  26321  jensen  26322  amgm  26324  lgamgulmlem2  26363  ftalem5  26410  efnnfsumcl  26436  efchtdvds  26492  dvdsmulf1o  26527  fsumdvdsmul  26528  lgsfcl2  26635  2sqlem6  26755  2sqlem8  26758  2sqlem9  26759  rpvmasumlem  26819  rpvmasum2  26844  dchrisum0re  26845  dchrisum0lem3  26851  dchrisum0  26852  rplogsum  26859  dirith2  26860  noextendseq  26999  oldf  27171  leftssno  27194  rightssno  27195  axtgcgrrflx  27290  axtgcgrid  27291  axtgsegcon  27292  axtg5seg  27293  axtgbtwnid  27294  axtgpasch  27295  axtgcont1  27296  tgcgr4  27359  motcgrg  27372  tglng  27374  upgrss  27925  pthdivtx  28563  disjxwwlkn  28744  ex-fpar  29292  nmlno0lem  29621  hlimcaui  30064  chsspwh  30075  shsss  30141  chintcli  30159  shsleji  30198  shub1i  30202  shsval2i  30215  lejdii  30366  spanuni  30372  sshhococi  30374  spansnpji  30406  osumcori  30471  5oai  30489  3oalem6  30495  3oai  30496  pjssmii  30509  mayete3i  30556  mayetes3i  30557  nmlnop0iALT  30823  imaelshi  30886  pjnmopi  30976  pjclem1  31023  pjci  31028  mdslmd1lem1  31153  shatomistici  31189  hatomistici  31190  chpssati  31191  xppreima  31448  iundisjfi  31582  iundisj2fi  31583  fprodex01  31604  xrsmulgzz  31752  fsumrp0cl  31769  gsummpt2co  31773  cycpmfv2  31846  cycpmrn  31875  1fldgenq  31972  xrge0slmod  32023  lsmsnorb  32055  idlsrgbas  32125  idlsrgplusg  32126  idlsrgmulr  32128  idlsrgtset  32129  ordtconnlem1  32374  xrge0iifhom  32387  lmlimxrge0  32398  lmxrge0  32402  indsumin  32490  esumcst  32531  esumpfinvallem  32542  esumpfinval  32543  esumpfinvalf  32544  esumcvg  32554  imambfm  32731  elmbfmvol2  32736  sxbrsigalem3  32741  sxbrsigalem2  32755  sxbrsigalem4  32756  sitgclg  32811  eulerpartlem1  32836  eulerpartlemgvv  32845  eulerpartlemgh  32847  eulerpartlemgf  32848  ballotlemfc0  32961  ballotlemfcc  32962  ballotlemiex  32970  ballotlemsup  32973  ballotlemsima  32984  ballotlemrv2  32990  ballotth  33006  signsplypnf  33031  signsply0  33032  rpsqrtcn  33075  itgexpif  33088  fsum2dsub  33089  reprfi2  33105  chtvalz  33111  breprexplemc  33114  breprexpnat  33116  circlemeth  33122  circlemethnat  33123  circlevma  33124  circlemethhgt  33125  hgt750lemd  33130  hgt750lema  33139  tgoldbachgtde  33142  tgoldbachgtda  33143  tgoldbachgt  33145  bnj1145  33474  bnj1286  33500  subfacp1lem2a  33643  erdszelem4  33657  erdszelem5  33658  erdszelem7  33660  erdszelem8  33661  kur14lem7  33675  kur14lem9  33677  cvxpconn  33705  cvxsconn  33706  resconn  33709  iccllysconn  33713  txpss3v  34430  txprel  34431  limitssson  34463  finminlem  34757  tailf  34814  filnetlem3  34819  onint1  34888  bj-unrab  35363  bj-2upln1upl  35462  bj-imdirco  35628  bj-rvecssabl  35744  taupilem2  35760  taupi  35761  poimirlem3  36048  poimirlem30  36075  poimirlem31  36076  poimirlem32  36077  broucube  36079  opnmbllem0  36081  mblfinlem1  36082  mblfinlem2  36083  mblfinlem3  36084  mblfinlem4  36085  ismblfin  36086  mbfposadd  36092  cnambfre  36093  itg2addnc  36099  ftc1cnnclem  36116  ftc1cnnc  36117  ftc1anclem3  36120  ftc1anclem7  36124  ftc1anc  36126  ftc2nc  36127  dvreasin  36131  dvreacos  36132  areacirclem1  36133  areacirclem2  36134  areacirc  36138  caures  36186  reheibor  36265  xrnss3v  36801  xrnrel  36802  atlatmstc  37748  atlatle  37749  pmaple  38191  sspadd1  38245  sspadd2  38246  dvrelog2  40488  dvrelog3  40489  ressbasss2  40635  diophin  41033  4rexfrabdioph  41059  6rexfrabdioph  41060  irrapxlem1  41083  irrapx1  41089  rmxyelqirr  41171  monotuz  41203  jm2.27dlem5  41275  hbtlem2  41389  algbase  41443  algaddg  41444  algmulr  41445  algsca  41446  algvsca  41447  arearect  41487  areaquad  41488  rtrclex  41831  trclubgNEW  41832  trclexi  41834  rtrclexi  41835  cnvtrcl0  41840  dfrtrcl5  41843  trrelsuperrel2dg  41885  relexpaddss  41932  brtrclfv2  41941  frege131d  41978  xphe  41995  clsk3nimkb  42254  gneispace  42348  k0004val0  42368  inaex  42519  lhe4.4ex1a  42551  uzmptshftfval  42568  binomcxplemdvbinom  42575  binomcxplemcvg  42576  binomcxplemnotnn0  42578  relopabVD  43125  fzisoeu  43470  fzsscn  43481  fzssre  43484  fzossuz  43551  zssxr  43568  uzssre2  43578  supminfxr  43635  uzsscn  43647  rpssxr  43652  uzinico  43730  limcresiooub  43815  limcresioolb  43816  limcleqr  43817  limclner  43824  limclr  43828  limsupequzmpt2  43891  liminfval2  43941  liminfequzmpt2  43964  icccncfext  44060  cncficcgt0  44061  ioodvbdlimc1lem2  44105  ioodvbdlimc2lem  44107  dvnprodlem1  44119  dvnprodlem2  44120  itgsin0pilem1  44123  itgsinexplem1  44127  itgsinexp  44128  dirkercncflem2  44277  fourierdlem16  44296  fourierdlem18  44298  fourierdlem20  44300  fourierdlem21  44301  fourierdlem22  44302  fourierdlem25  44305  fourierdlem37  44317  fourierdlem42  44322  fourierdlem50  44329  fourierdlem52  44331  fourierdlem62  44341  fourierdlem64  44343  fourierdlem66  44345  fourierdlem68  44347  fourierdlem74  44353  fourierdlem75  44354  fourierdlem76  44355  fourierdlem79  44358  fourierdlem83  44362  fourierdlem95  44374  fourierdlem101  44380  fourierdlem102  44381  fourierdlem103  44382  fourierdlem104  44383  fourierdlem112  44391  fourierdlem114  44393  sqwvfoura  44401  sqwvfourb  44402  fouriersw  44404  etransclem24  44431  etransclem48  44455  sge0sn  44552  sge0tsms  44553  sge0f1o  44555  sge0pr  44567  sge0resplit  44579  sge0split  44582  sge0iunmptlemre  44588  sge0isummpt2  44605  carageniuncllem1  44694  hoicvr  44721  hoicvrrex  44729  hoidmvlelem2  44769  hspmbl  44802  smfmullem4  44967  prmdvdsfmtnof1lem1  45708  prmdvdsfmtnof  45710  oddibas  46039  2zrngbas  46166  2zrng0  46168  sepfsepc  46892  aacllem  47180  amgmlemALT  47182