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

This proof depends on syntax axioms:   ⊆ wss 3899

This proof depends on axioms:  ax-mp 5  ax-1 6  ax-2 7  ax-3 8  ax-gen 1828  ax-4 1842

This proof depends on definitions:  df-bi 210  df-ss 3916

This theorem is used by:  snsstp1  4777  snsstp2  4778  uniintsn  4945  elopabran  5540  ssrnres  6171  cossxp  6269  foimacnv  6836  ssimaex  6964  riotassuni  7411  oprabss  7522  dmexg  7899  rnexg  7900  mptmpoopabbrd  8081  fparlem3  8112  fparlem4  8113  snopsuppss  8178  tposssxp  8229  naddunif  8685  naddasslem1  8686  naddasslem2  8687  mapsspw  8888  sbthlem5  9092  sbthlem7  9094  cnvimamptfin  9323  marypha1lem  9406  ordtypelem4  9496  hartogslem1  9517  ttrclco  9700  cottrcl  9701  tc2  9722  frmin  9734  frrlem16  9743  tz9.12lem1  9772  rankval4  9852  rankxpl  9860  rankmapu  9863  rankxplim  9864  djuin  9926  infxpenlem  10019  ackbij1lem18  10241  cflm  10254  fin23lem29  10346  hsmexlem4  10434  hsmexlem5  10435  brdom3  10534  brdom5  10535  brdom4  10536  smobeth  10598  pwfseqlem3  10672  wundm  10740  wunrn  10741  wunex2  10750  ltsopi  10900  dmaddpi  10902  dmmulpi  10903  nqerf  10942  ltrelxr  11297  uzssre  12912  uzwo2  12964  infssuzle  12983  infssuzcl  12984  uzwo3  12995  nn0ssq  13009  nnssq  13010  qsscn  13012  rpnnen1lem3  13032  rpnnen1lem5  13034  dflt2  13202  ioosscn  13464  unitsscn  13556  fzval2  13567  fzossz  13738  fzossnn  13770  injresinj  13850  flval3  13879  uzsup  13927  uzrdgfni  14025  expcl2lem  14140  rpexpcl  14147  expge0  14165  expge1  14166  hashxrcl  14424  seqcoll  14532  xptrrel  15056  trclublem  15071  01sqrexlem3  15334  limsupval2  15570  limsupgre  15571  rlimpm  15590  rlimclim  15636  isercolllem1  15755  isercolllem2  15756  isercoll  15758  caurcvg  15767  caucvg  15769  summolem2a  15804  summolem2  15805  zsum  15807  fsumcvg3  15818  fsumrpcl  15826  fsumge0  15885  climfsum  15910  ackbijnn  15920  prodmolem2a  16024  prodmolem2  16025  zprod  16027  fprodrpcl  16046  fprodge0  16083  fprodge1  16085  rprisefaccl  16113  divalglem8  16493  sadaddlem  16559  lcmfval  16714  isprm3  16776  maxprmfct  16803  pclem  16933  prmreclem1  17011  prmreclem2  17012  prmreclem3  17013  1arith  17022  4sqlem11  17050  ramtlecl  17095  ramcl2lem  17104  ramxrcl  17112  prmgaplem3  17148  prmgaplem4  17149  cshwshashlem1  17190  structfn  17251  strleun  17252  ressbasss  17334  ressbasss2  17336  srngbase  17398  srngplusg  17399  srngmulr  17400  lmodbase  17414  lmodplusg  17415  lmodsca  17416  ipsbase  17425  ipsaddg  17426  ipsmulr  17427  ipssca  17428  ipsvsca  17429  ipsip  17430  phlbase  17435  phlplusg  17436  phlsca  17437  phlvsca  17438  phlip  17439  odrngbas  17492  odrngplusg  17493  odrngmulr  17494  odrngtset  17495  odrngle  17496  odrngds  17497  prdsvallem  17542  prdsval  17543  prdssca  17544  prdsbas  17545  prdsplusg  17546  prdsmulr  17547  prdsvsca  17548  prdsip  17549  prdsle  17550  prdsds  17552  prdstset  17554  prdshom  17555  prdsco  17556  imasbas  17601  imasds  17602  imasplusg  17606  imasmulr  17607  imassca  17608  imasvsca  17609  imasip  17610  imastset  17611  imasle  17612  wunfunc  17993  fullfunc  18000  fthfunc  18001  isfull  18004  isfth  18008  wunnat  18051  dmcoass  18158  catcisolem  18202  catciso  18203  catcoppccl  18209  catcfuccl  18210  catcxpccl  18298  ipobas  18622  ipolerval  18623  ipotset  18624  psdmrn  18664  psss  18671  ledm  18681  lern  18682  dirdm  18691  dirge  18694  mulgfval  19195  mvdco  19575  f1omvdconj  19576  gexex  19983  gsumval3  20037  lssacs  21154  cnfldbas  21592  mpocnfldadd  21593  mpocnfldmul  21595  cnfldcj  21597  cnfldtset  21598  cnfldle  21599  cnfldds  21600  cnfldunif  21601  rge0srg  21654  zntoslem  21772  asplss  22091  aspsubrg  22093  psrass1lem  22151  psrbas  22152  psrplusg  22155  psrmulr  22160  psrsca  22165  psrvscafval  22166  psrass1  22181  psrass23l  22184  psrcom  22185  psrass23  22186  psropprmul  22465  coe1mul2  22498  ofco2  22676  toponsspwpw  23150  dmtopon  23151  leordtval2  23440  lmbrf  23488  lmres  23528  fiuncmp  23632  comppfsc  23761  1stckgenlem  23782  kgencn3  23787  ptbasfi  23810  xkoopn  23818  txcnmpt  23853  txkgen  23881  opnfbas  24071  fmfnfmlem4  24186  tsmsxplem1  24382  trust  24458  restutop  24466  nmoffn  24940  nmofval  24943  nmogelb  24945  nmolb  24946  nmof  24948  qtopbas  24988  tgqioo  25029  re2ndc  25030  iitopon  25110  dfii3  25114  cnheiborlem  25185  bndth  25189  lebnumii  25197  pcoass  25255  cphsqrtcl  25415  lmmbrf  25493  iscauf  25511  caucfil  25514  lmclimf  25535  rrxmval  25636  rrxmet  25639  ovolfioo  25698  ovolficc  25699  ovolficcss  25700  ovolfsf  25702  ovollb  25710  ovolicc2lem3  25750  ovolicc2lem4  25751  ovolicc2  25753  volf  25760  volsup  25787  ovolfs2  25802  uniiccdif  25809  uniioovol  25810  uniiccvol  25811  uniioombllem2  25814  uniioombllem3a  25815  uniioombllem3  25816  uniioombllem4  25817  uniioombllem5  25818  uniioombl  25820  dyadmbllem  25830  dyadmbl  25831  opnmbllem  25832  opnmblALT  25834  volsup2  25836  vitalilem4  25842  vitalilem5  25843  vitali  25844  mbfimaopnlem  25886  mbflimsup  25897  i1f0  25918  i1f1  25921  itg11  25922  itg2mulc  25978  itg2gt0  25991  ellimc2  26107  limcresi  26115  dvreslem  26139  dvres2lem  26140  dvaddbr  26168  dvmulbr  26169  dvlipcn  26224  c1liplem1  26226  lhop1lem  26243  lhop1  26244  lhop2  26245  lhop  26246  dvfsumrlim  26261  ftc1cn  26273  itgsubstlem  26278  itgsubst  26279  itgpowd  26280  mdegleb  26292  mdeglt  26293  mdegldg  26294  mdegxrcl  26295  mdegcl  26297  mdegaddle  26302  mdegmullem  26306  deg1mul3le  26345  ig1peu  26403  ig1pdvds  26408  aacjcl  26566  aannenlem2  26568  aannenlem3  26569  aalioulem2  26572  taylfval  26598  radcnvcl  26656  radcnvlt1  26657  radcnvle  26659  abelth  26680  abelth2  26681  pilem2  26691  pilem3  26692  pige3ALT  26760  recosf1o  26775  resinf1o  26776  tanord1  26777  logcn  26887  dvlog  26891  dvlog2lem  26892  efopn  26898  logtayl  26900  cxpcn3  26988  loglesqrt  27001  ssscongptld  27062  leibpi  27182  efrlim  27209  jensenlem1  27226  jensenlem2  27227  jensen  27228  amgm  27230  lgamgulmlem2  27269  ftalem5  27316  efnnfsumcl  27342  efchtdvds  27398  mpodvdsmulf1o  27433  fsumdvdsmul  27434  dvdsmulf1o  27435  lgsfcl2  27542  2sqlem6  27662  2sqlem8  27665  2sqlem9  27666  rpvmasumlem  27726  rpvmasum2  27751  dchrisum0re  27752  dchrisum0lem3  27758  dchrisum0  27759  rplogsum  27766  dirith2  27767  noextendseq  27906  oldf  28105  leftssno  28141  rightssno  28142  addbdaylem  28285  mulsproplem12  28395  mulsproplem13  28396  mulsproplem14  28397  mulsasslem3  28433  precsexlem11  28485  oncutlt  28532  bdayons  28544  nnssno  28590  axtgcgrrflx  28806  axtgcgrid  28807  axtgsegcon  28808  axtg5seg  28809  axtgbtwnid  28810  axtgpasch  28811  axtgcont1  28812  tgcgr4  28876  motcgrg  28889  tglng  28891  upgrss  29548  pthdivtx  30194  disjxwwlkn  30384  ex-fpar  30945  nmlno0lem  31277  hlimcaui  31720  chsspwh  31731  shsss  31797  chintcli  31815  shsleji  31854  shub1i  31858  shsval2i  31871  lejdii  32022  spanuni  32028  sshhococi  32030  spansnpji  32062  osumcori  32127  5oai  32145  3oalem6  32151  3oai  32152  pjssmii  32165  mayete3i  32212  mayetes3i  32213  nmlnop0iALT  32479  imaelshi  32542  pjnmopi  32632  pjclem1  32679  pjci  32684  mdslmd1lem1  32809  shatomistici  32845  hatomistici  32846  chpssati  32847  xppreima  33121  iundisjfi  33270  iundisj2fi  33271  fprodex01  33298  indsumin  33310  xrsmulgzz  33452  fsumrp0cl  33464  gsummpt2co  33491  cycpmfv2  33557  cycpmrn  33586  rlocbas  33711  rlocaddval  33712  rlocmulval  33713  1fldgenq  33766  xrge0slmod  33791  lsmsnorb  33827  idlsrgbas  33917  idlsrgplusg  33918  idlsrgmulr  33920  idlsrgtset  33921  selvply1rhmlemb  34032  esplyind  34088  vietalem  34092  constrextdg2  34262  ordtconnlem1  34437  xrge0iifhom  34450  lmlimxrge0  34461  lmxrge0  34465  esumcst  34576  esumpfinvallem  34587  esumpfinval  34588  esumpfinvalf  34589  esumcvg  34599  imambfm  34776  elmbfmvol2  34781  sxbrsigalem3  34786  sxbrsigalem2  34800  sxbrsigalem4  34801  sitgclg  34856  eulerpartlem1  34881  eulerpartlemgvv  34890  eulerpartlemgh  34892  eulerpartlemgf  34893  ballotlemfc0  35007  ballotlemfcc  35008  ballotlemiex  35016  ballotlemsup  35019  ballotlemsima  35030  ballotlemrv2  35036  ballotth  35052  signsplypnf  35061  signsply0  35062  rpsqrtcn  35104  itgexpif  35117  fsum2dsub  35118  reprfi2  35134  chtvalz  35140  breprexplemc  35143  breprexpnat  35145  circlemeth  35151  circlemethnat  35152  circlevma  35153  circlemethhgt  35154  hgt750lemd  35159  hgt750lema  35168  tgoldbachgtde  35171  tgoldbachgtda  35172  tgoldbachgt  35174  bnj1145  35505  bnj1286  35531  subfacp1lem2a  35762  erdszelem4  35776  erdszelem5  35777  erdszelem7  35779  erdszelem8  35780  kur14lem7  35794  kur14lem9  35796  resconn  35828  iccllysconn  35832  txpss3v  36458  txprel  36459  limitssson  36491  finminlem  36940  tailf  36997  filnetlem3  37002  onint1  37071  ttcuniun  37132  bj-unrab  37673  bj-2upln1upl  37771  bj-imdirco  37945  bj-rvecssabl  38061  taupilem2  38077  taupi  38078  poimirlem3  38375  poimirlem30  38402  poimirlem31  38403  poimirlem32  38404  broucube  38406  opnmbllem0  38408  mblfinlem1  38409  mblfinlem2  38410  mblfinlem3  38411  mblfinlem4  38412  ismblfin  38413  mbfposadd  38419  cnambfre  38420  itg2addnc  38426  ftc1cnnclem  38443  ftc1cnnc  38444  ftc1anclem3  38447  ftc1anclem7  38451  ftc1anc  38453  ftc2nc  38454  dvreasin  38458  dvreacos  38459  areacirclem1  38460  areacirclem2  38461  areacirc  38465  caures  38513  reheibor  38592  xrnss3v  39132  xrnrel  39133  atlatmstc  40195  atlatle  40196  pmaple  40637  sspadd1  40691  sspadd2  40692  dvrelog2  42933  dvrelog3  42934  rpsscn  43177  sumcubes  43191  redvmptabs  43238  diophin  43620  4rexfrabdioph  43642  6rexfrabdioph  43643  irrapxlem1  43666  irrapx1  43672  rmxyelqirr  43754  monotuz  43785  jm2.27dlem5  43857  hbtlem2  43968  algbase  44018  algaddg  44019  algmulr  44020  algsca  44021  algvsca  44022  arearect  44059  areaquad  44060  rtrclex  44460  trclubgNEW  44461  trclexi  44463  rtrclexi  44464  cnvtrcl0  44469  dfrtrcl5  44472  trrelsuperrel2dg  44514  relexpaddss  44561  brtrclfv2  44570  frege131d  44607  xphe  44624  clsk3nimkb  44883  gneispace  44977  k0004val0  44997  inaex  45124  lhe4.4ex1a  45156  uzmptshftfval  45173  binomcxplemdvbinom  45180  binomcxplemcvg  45181  binomcxplemnotnn0  45183  relopabVD  45726  dmwf  45791  rnwf  45792  fzisoeu  46136  fzsscn  46147  fzssre  46150  fzossuz  46213  zssxr  46229  uzssre2  46238  supminfxr  46295  uzsscn  46306  rpssxr  46311  uzinico  46392  limcresiooub  46473  limcresioolb  46474  limcleqr  46475  limclner  46482  limclr  46486  limsupequzmpt2  46549  liminfval2  46599  liminfequzmpt2  46622  icccncfext  46718  cncficcgt0  46719  ioodvbdlimc1lem2  46763  ioodvbdlimc2lem  46765  dvnprodlem2  46778  itgsin0pilem1  46781  itgsinexplem1  46785  itgsinexp  46786  dirkercncflem2  46935  fourierdlem16  46954  fourierdlem18  46956  fourierdlem20  46958  fourierdlem21  46959  fourierdlem22  46960  fourierdlem25  46963  fourierdlem37  46975  fourierdlem42  46980  fourierdlem50  46987  fourierdlem52  46989  fourierdlem62  46999  fourierdlem64  47001  fourierdlem66  47003  fourierdlem68  47005  fourierdlem74  47011  fourierdlem75  47012  fourierdlem76  47013  fourierdlem79  47016  fourierdlem83  47020  fourierdlem95  47032  fourierdlem101  47038  fourierdlem102  47039  fourierdlem103  47040  fourierdlem104  47041  fourierdlem112  47049  fourierdlem114  47051  sqwvfoura  47059  sqwvfourb  47060  fouriersw  47062  etransclem24  47089  etransclem48  47113  sge0sn  47210  sge0tsms  47211  sge0f1o  47213  sge0pr  47225  sge0resplit  47237  sge0split  47240  sge0iunmptlemre  47246  sge0isummpt2  47263  carageniuncllem1  47352  hoicvr  47379  hoicvrrex  47387  hoidmvlelem2  47427  hspmbl  47460  smfmullem4  47625  chnsuslle  47712  lamberte  47759  rehalfge1  48230  prmdvdsfmtnof1lem1  48490  prmdvdsfmtnof  48492  upgrimpthslem2  48827  upgrimpths  48828  oddibas  49091  2zrngbas  49160  2zrng0  49162  dmtposss  49805  tposres3  49810  sepfsepc  49857  uptrlem1  50139  uptrlem2  50140  uptrlem3  50141  uptra  50144  uptrar  50145  uobeqw  50148  uptr2  50150  uptr2a  50151  fucoppcfunc  50341  aacllem  50775  amgmlemALT  50824