Theorem sstri 3940

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

Syntax hints:   ⊆ wss 3898

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

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

This theorem is referenced by:  snsstp1  4769  snsstp2  4770  uniintsn  4937  elopabran  5506  ssrnres  6132  cossxp  6226  foimacnv  6787  ssimaex  6915  riotassuni  7351  oprabss  7462  dmexg  7839  rnexg  7840  fabexgOLD  7877  mptmpoopabbrd  8020  fparlem3  8052  fparlem4  8053  snopsuppss  8117  tposssxp  8168  naddunif  8616  naddasslem1  8617  naddasslem2  8618  mapsspw  8810  sbthlem5  9013  sbthlem7  9015  cnvimamptfin  9246  marypha1lem  9326  ordtypelem4  9416  hartogslem1  9437  ttrclco  9617  cottrcl  9618  tc2  9639  frmin  9651  frrlem16  9660  tz9.12lem1  9689  rankval4  9769  rankxpl  9777  rankmapu  9780  rankxplim  9781  djuin  9820  infxpenlem  9913  ackbij1lem18  10136  cflm  10150  fin23lem29  10241  hsmexlem4  10329  hsmexlem5  10330  brdom3  10428  brdom5  10429  brdom4  10430  smobeth  10486  pwfseqlem3  10560  wundm  10628  wunrn  10629  wunex2  10638  ltsopi  10788  dmaddpi  10790  dmmulpi  10791  nqerf  10830  ltrelxr  11182  uzssre  12762  uzwo2  12814  infssuzle  12833  infssuzcl  12834  uzwo3  12845  nn0ssq  12859  nnssq  12860  qsscn  12862  rpnnen1lem3  12881  rpnnen1lem5  12883  dflt2  13051  ioosscn  13312  unitsscn  13404  fzval2  13414  fzossz  13583  fzossnn  13615  injresinj  13695  flval3  13723  uzsup  13771  uzrdgfni  13869  expcl2lem  13984  rpexpcl  13991  expge0  14009  expge1  14010  hashxrcl  14268  seqcoll  14375  xptrrel  14891  trclublem  14906  01sqrexlem3  15155  limsupval2  15391  limsupgre  15392  rlimpm  15411  rlimclim  15457  isercolllem1  15576  isercolllem2  15577  isercoll  15579  caurcvg  15588  caucvg  15590  summolem2a  15626  summolem2  15627  zsum  15629  fsumcvg3  15640  fsumrpcl  15648  fsumge0  15706  climfsum  15731  ackbijnn  15739  prodmolem2a  15845  prodmolem2  15846  zprod  15848  fprodrpcl  15867  fprodge0  15904  fprodge1  15906  rprisefaccl  15934  divalglem8  16315  sadaddlem  16381  lcmfval  16536  isprm3  16598  maxprmfct  16624  pclem  16754  prmreclem1  16832  prmreclem2  16833  prmreclem3  16834  1arith  16843  4sqlem11  16871  ramtlecl  16916  ramcl2lem  16925  ramxrcl  16933  prmgaplem3  16969  prmgaplem4  16970  cshwshashlem1  17011  structfn  17071  strleun  17072  ressbasss  17154  ressbasss2  17156  srngbase  17218  srngplusg  17219  srngmulr  17220  lmodbase  17234  lmodplusg  17235  lmodsca  17236  ipsbase  17245  ipsaddg  17246  ipsmulr  17247  ipssca  17248  ipsvsca  17249  ipsip  17250  phlbase  17255  phlplusg  17256  phlsca  17257  phlvsca  17258  phlip  17259  odrngbas  17312  odrngplusg  17313  odrngmulr  17314  odrngtset  17315  odrngle  17316  odrngds  17317  prdsvallem  17362  prdsval  17363  prdssca  17364  prdsbas  17365  prdsplusg  17366  prdsmulr  17367  prdsvsca  17368  prdsip  17369  prdsle  17370  prdsds  17372  prdstset  17374  prdshom  17375  prdsco  17376  imasbas  17420  imasds  17421  imasplusg  17425  imasmulr  17426  imassca  17427  imasvsca  17428  imasip  17429  imastset  17430  imasle  17431  wunfunc  17812  fullfunc  17819  fthfunc  17820  isfull  17823  isfth  17827  wunnat  17870  dmcoass  17977  catcisolem  18021  catciso  18022  catcoppccl  18028  catcfuccl  18029  catcxpccl  18117  ipobas  18441  ipolerval  18442  ipotset  18443  psdmrn  18483  psss  18490  ledm  18500  lern  18501  dirdm  18510  dirge  18513  mulgfval  18986  mvdco  19361  f1omvdconj  19362  gexex  19769  gsumval3  19823  lssacs  20904  cnfldbas  21299  mpocnfldadd  21300  mpocnfldmul  21302  cnfldcj  21304  cnfldtset  21305  cnfldle  21306  cnfldds  21307  cnfldunif  21308  cnfldbasOLD  21314  cnfldaddOLD  21315  cnfldmulOLD  21316  cnfldcjOLD  21317  cnfldtsetOLD  21318  cnfldleOLD  21319  cnflddsOLD  21320  cnfldunifOLD  21321  rge0srg  21379  zntoslem  21497  asplss  21815  aspsubrg  21817  psrass1lem  21873  psrbas  21874  psrplusg  21877  psrmulr  21883  psrsca  21888  psrvscafval  21889  psrass1  21904  psrass23l  21907  psrcom  21908  psrass23  21909  psropprmul  22153  coe1mul2  22186  ofco2  22369  toponsspwpw  22840  dmtopon  22841  leordtval2  23130  lmbrf  23178  lmres  23218  fiuncmp  23322  comppfsc  23450  1stckgenlem  23471  kgencn3  23476  ptbasfi  23499  xkoopn  23507  txcnmpt  23542  txkgen  23570  opnfbas  23760  fmfnfmlem4  23875  tsmsxplem1  24071  trust  24147  restutop  24155  nmoffn  24629  nmofval  24632  nmogelb  24634  nmolb  24635  nmof  24637  qtopbas  24677  tgqioo  24718  re2ndc  24719  iitopon  24802  dfii3  24806  iimulcnOLD  24865  cnheiborlem  24883  bndth  24887  lebnumii  24895  reparphtiOLD  24927  pcoass  24954  cphsqrtcl  25114  lmmbrf  25192  iscauf  25210  caucfil  25213  lmclimf  25234  rrxmval  25335  rrxmet  25338  ovolfioo  25398  ovolficc  25399  ovolficcss  25400  ovolfsf  25402  ovollb  25410  ovolicc2lem3  25450  ovolicc2lem4  25451  ovolicc2  25453  volf  25460  volsup  25487  ovolfs2  25502  uniiccdif  25509  uniioovol  25510  uniiccvol  25511  uniioombllem2  25514  uniioombllem3a  25515  uniioombllem3  25516  uniioombllem4  25517  uniioombllem5  25518  uniioombl  25520  dyadmbllem  25530  dyadmbl  25531  opnmbllem  25532  opnmblALT  25534  volsup2  25536  vitalilem4  25542  vitalilem5  25543  vitali  25544  mbfimaopnlem  25586  mbflimsup  25597  i1f0  25618  i1f1  25621  itg11  25622  itg2mulc  25678  itg2gt0  25691  ellimc2  25808  limcresi  25816  dvreslem  25840  dvres2lem  25841  dvaddbr  25870  dvmulbr  25871  dvmulbrOLD  25872  dvlipcn  25929  c1liplem1  25931  lhop1lem  25948  lhop1  25949  lhop2  25950  lhop  25951  dvfsumrlim  25968  ftc1cn  25980  itgsubstlem  25985  itgsubst  25986  itgpowd  25987  mdegleb  25999  mdeglt  26000  mdegldg  26001  mdegxrcl  26002  mdegcl  26004  mdegaddle  26009  mdegmullem  26013  deg1mul3le  26052  ig1peu  26110  ig1pdvds  26115  aacjcl  26265  aannenlem2  26267  aannenlem3  26268  aalioulem2  26271  taylfval  26296  radcnvcl  26356  radcnvlt1  26357  radcnvle  26359  abelth  26381  abelth2  26382  pilem2  26392  pilem3  26393  pige3ALT  26459  recosf1o  26474  resinf1o  26475  tanord1  26476  logcn  26586  dvlog  26590  dvlog2lem  26591  efopn  26597  logtayl  26599  cxpcn3  26688  loglesqrt  26701  ssscongptld  26762  leibpi  26882  efrlim  26909  efrlimOLD  26910  jensenlem1  26927  jensenlem2  26928  jensen  26929  amgm  26931  lgamgulmlem2  26970  ftalem5  27017  efnnfsumcl  27043  efchtdvds  27099  mpodvdsmulf1o  27134  fsumdvdsmul  27135  dvdsmulf1o  27136  fsumdvdsmulOLD  27137  lgsfcl2  27244  2sqlem6  27364  2sqlem8  27367  2sqlem9  27368  rpvmasumlem  27428  rpvmasum2  27453  dchrisum0re  27454  dchrisum0lem3  27460  dchrisum0  27461  rplogsum  27468  dirith2  27469  noextendseq  27609  oldf  27801  leftssno  27829  rightssno  27830  addsbdaylem  27962  mulsproplem12  28069  mulsproplem13  28070  mulsproplem14  28071  mulsasslem3  28107  precsexlem11  28158  onscutlt  28204  bdayon  28212  nnssno  28254  axtgcgrrflx  28443  axtgcgrid  28444  axtgsegcon  28445  axtg5seg  28446  axtgbtwnid  28447  axtgpasch  28448  axtgcont1  28449  tgcgr4  28512  motcgrg  28525  tglng  28527  upgrss  29070  pthdivtx  29709  disjxwwlkn  29895  ex-fpar  30446  nmlno0lem  30777  hlimcaui  31220  chsspwh  31231  shsss  31297  chintcli  31315  shsleji  31354  shub1i  31358  shsval2i  31371  lejdii  31522  spanuni  31528  sshhococi  31530  spansnpji  31562  osumcori  31627  5oai  31645  3oalem6  31651  3oai  31652  pjssmii  31665  mayete3i  31712  mayetes3i  31713  nmlnop0iALT  31979  imaelshi  32042  pjnmopi  32132  pjclem1  32179  pjci  32184  mdslmd1lem1  32309  shatomistici  32345  hatomistici  32346  chpssati  32347  xppreima  32631  iundisjfi  32785  iundisj2fi  32786  fprodex01  32815  indsumin  32852  xrsmulgzz  32999  fsumrp0cl  33011  gsummpt2co  33037  cycpmfv2  33092  cycpmrn  33121  rlocbas  33243  rlocaddval  33244  rlocmulval  33245  1fldgenq  33297  xrge0slmod  33322  lsmsnorb  33365  idlsrgbas  33478  idlsrgplusg  33479  idlsrgmulr  33481  idlsrgtset  33482  esplyind  33615  constrextdg2  33785  ordtconnlem1  33960  xrge0iifhom  33973  lmlimxrge0  33984  lmxrge0  33988  esumcst  34099  esumpfinvallem  34110  esumpfinval  34111  esumpfinvalf  34112  esumcvg  34122  imambfm  34298  elmbfmvol2  34303  sxbrsigalem3  34308  sxbrsigalem2  34322  sxbrsigalem4  34323  sitgclg  34378  eulerpartlem1  34403  eulerpartlemgvv  34412  eulerpartlemgh  34414  eulerpartlemgf  34415  ballotlemfc0  34529  ballotlemfcc  34530  ballotlemiex  34538  ballotlemsup  34541  ballotlemsima  34552  ballotlemrv2  34558  ballotth  34574  signsplypnf  34586  signsply0  34587  rpsqrtcn  34629  itgexpif  34642  fsum2dsub  34643  reprfi2  34659  chtvalz  34665  breprexplemc  34668  breprexpnat  34670  circlemeth  34676  circlemethnat  34677  circlevma  34678  circlemethhgt  34679  hgt750lemd  34684  hgt750lema  34693  tgoldbachgtde  34696  tgoldbachgtda  34697  tgoldbachgt  34699  bnj1145  35028  bnj1286  35054  subfacp1lem2a  35247  erdszelem4  35261  erdszelem5  35262  erdszelem7  35264  erdszelem8  35265  kur14lem7  35279  kur14lem9  35281  resconn  35313  iccllysconn  35317  txpss3v  35943  txprel  35944  limitssson  35976  finminlem  36385  tailf  36442  filnetlem3  36447  onint1  36516  bj-unrab  36993  bj-2upln1upl  37091  bj-imdirco  37257  bj-rvecssabl  37373  taupilem2  37389  taupi  37390  poimirlem3  37686  poimirlem30  37713  poimirlem31  37714  poimirlem32  37715  broucube  37717  opnmbllem0  37719  mblfinlem1  37720  mblfinlem2  37721  mblfinlem3  37722  mblfinlem4  37723  ismblfin  37724  mbfposadd  37730  cnambfre  37731  itg2addnc  37737  ftc1cnnclem  37754  ftc1cnnc  37755  ftc1anclem3  37758  ftc1anclem7  37762  ftc1anc  37764  ftc2nc  37765  dvreasin  37769  dvreacos  37770  areacirclem1  37771  areacirclem2  37772  areacirc  37776  caures  37823  reheibor  37902  xrnss3v  38428  xrnrel  38429  atlatmstc  39441  atlatle  39442  pmaple  39883  sspadd1  39937  sspadd2  39938  dvrelog2  42180  dvrelog3  42181  rpsscn  42420  sumcubes  42434  redvmptabs  42481  diophin  42892  4rexfrabdioph  42918  6rexfrabdioph  42919  irrapxlem1  42942  irrapx1  42948  rmxyelqirr  43030  monotuz  43061  jm2.27dlem5  43133  hbtlem2  43244  algbase  43294  algaddg  43295  algmulr  43296  algsca  43297  algvsca  43298  arearect  43335  areaquad  43336  rtrclex  43737  trclubgNEW  43738  trclexi  43740  rtrclexi  43741  cnvtrcl0  43746  dfrtrcl5  43749  trrelsuperrel2dg  43791  relexpaddss  43838  brtrclfv2  43847  frege131d  43884  xphe  43901  clsk3nimkb  44160  gneispace  44254  k0004val0  44274  inaex  44417  lhe4.4ex1a  44449  uzmptshftfval  44466  binomcxplemdvbinom  44473  binomcxplemcvg  44474  binomcxplemnotnn0  44476  relopabVD  45020  dmwf  45085  rnwf  45086  fzisoeu  45428  fzsscn  45439  fzssre  45442  fzossuz  45506  zssxr  45522  uzssre2  45532  supminfxr  45589  uzsscn  45600  rpssxr  45605  uzinico  45686  limcresiooub  45767  limcresioolb  45768  limcleqr  45769  limclner  45776  limclr  45780  limsupequzmpt2  45843  liminfval2  45893  liminfequzmpt2  45916  icccncfext  46012  cncficcgt0  46013  ioodvbdlimc1lem2  46057  ioodvbdlimc2lem  46059  dvnprodlem2  46072  itgsin0pilem1  46075  itgsinexplem1  46079  itgsinexp  46080  dirkercncflem2  46229  fourierdlem16  46248  fourierdlem18  46250  fourierdlem20  46252  fourierdlem21  46253  fourierdlem22  46254  fourierdlem25  46257  fourierdlem37  46269  fourierdlem42  46274  fourierdlem50  46281  fourierdlem52  46283  fourierdlem62  46293  fourierdlem64  46295  fourierdlem66  46297  fourierdlem68  46299  fourierdlem74  46305  fourierdlem75  46306  fourierdlem76  46307  fourierdlem79  46310  fourierdlem83  46314  fourierdlem95  46326  fourierdlem101  46332  fourierdlem102  46333  fourierdlem103  46334  fourierdlem104  46335  fourierdlem112  46343  fourierdlem114  46345  sqwvfoura  46353  sqwvfourb  46354  fouriersw  46356  etransclem24  46383  etransclem48  46407  sge0sn  46504  sge0tsms  46505  sge0f1o  46507  sge0pr  46519  sge0resplit  46531  sge0split  46534  sge0iunmptlemre  46540  sge0isummpt2  46557  carageniuncllem1  46646  hoicvr  46673  hoicvrrex  46681  hoidmvlelem2  46721  hspmbl  46754  smfmullem4  46919  chnsuslle  47006  lamberte  47015  rehalfge1  47462  prmdvdsfmtnof1lem1  47711  prmdvdsfmtnof  47713  upgrimpthslem2  48035  upgrimpths  48036  oddibas  48300  2zrngbas  48369  2zrng0  48371  dmtposss  49003  tposres3  49008  sepfsepc  49055  uptrlem1  49338  uptrlem2  49339  uptrlem3  49340  uptra  49343  uptrar  49344  uobeqw  49347  uptr2  49349  uptr2a  49350  fucoppcfunc  49540  aacllem  49929  amgmlemALT  49931