Theorem sstri 3926

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

Syntax hints:   ⊆ wss 3883

This theorem was proved from axioms:  ax-mp 5  ax-1 6  ax-2 7  ax-3 8  ax-gen 1799  ax-4 1813  ax-5 1914  ax-6 1972  ax-7 2012  ax-8 2110  ax-9 2118  ax-ext 2709

This theorem depends on definitions:  df-bi 206  df-an 396  df-tru 1542  df-ex 1784  df-sb 2069  df-clab 2716  df-cleq 2730  df-clel 2817  df-v 3424  df-in 3890  df-ss 3900

This theorem is referenced by:  snsstp1  4746  snsstp2  4747  uniintsn  4915  ssrnres  6070  cossxp  6164  foimacnv  6717  ssimaex  6835  riotassuni  7253  oprabss  7359  dmexg  7724  rnexg  7725  fabexg  7755  fparlem3  7925  fparlem4  7926  snopsuppss  7966  tposssxp  8017  mapsspw  8624  sbthlem5  8827  sbthlem7  8829  cnvimamptfin  9050  marypha1lem  9122  ordtypelem4  9210  hartogslem1  9231  tc2  9431  tz9.12lem1  9476  rankval4  9556  rankxpl  9564  rankmapu  9567  rankxplim  9568  djuin  9607  infxpenlem  9700  ackbij1lem18  9924  cflm  9937  fin23lem29  10028  hsmexlem4  10116  hsmexlem5  10117  brdom3  10215  brdom5  10216  brdom4  10217  smobeth  10273  pwfseqlem3  10347  wundm  10415  wunrn  10416  wunex2  10425  ltsopi  10575  dmaddpi  10577  dmmulpi  10578  nqerf  10617  ltrelxr  10967  uzssre  12533  uzwo2  12581  infssuzle  12600  infssuzcl  12601  uzwo3  12612  nn0ssq  12626  nnssq  12627  qsscn  12629  rpnnen1lem3  12648  rpnnen1lem5  12650  dflt2  12811  ioosscn  13070  unitsscn  13161  fzval2  13171  fzossz  13335  fzossnn  13364  injresinj  13436  flval3  13463  uzsup  13511  uzrdgfni  13606  expcl2lem  13722  rpexpcl  13729  expge0  13747  expge1  13748  hashxrcl  14000  seqcoll  14106  xptrrel  14619  trclublem  14634  sqrlem3  14884  limsupval2  15117  limsupgre  15118  rlimpm  15137  rlimclim  15183  isercolllem1  15304  isercolllem2  15305  isercoll  15307  caurcvg  15316  caucvg  15318  summolem2a  15355  summolem2  15356  zsum  15358  fsumcvg3  15369  fsumrpcl  15377  fsumge0  15435  climfsum  15460  ackbijnn  15468  prodmolem2a  15572  prodmolem2  15573  zprod  15575  fprodrpcl  15594  fprodge0  15631  fprodge1  15633  rprisefaccl  15661  divalglem8  16037  sadaddlem  16101  lcmfval  16254  isprm3  16316  maxprmfct  16342  pclem  16467  prmreclem1  16545  prmreclem2  16546  prmreclem3  16547  1arith  16556  4sqlem11  16584  ramtlecl  16629  ramcl2lem  16638  ramxrcl  16646  prmgaplem3  16682  prmgaplem4  16683  cshwshashlem1  16725  structfn  16785  strleun  16786  srngbase  16946  srngplusg  16947  srngmulr  16948  lmodbase  16962  lmodplusg  16963  lmodsca  16964  ipsbase  16972  ipsaddg  16973  ipsmulr  16974  ipssca  16975  ipsvsca  16976  ipsip  16977  phlbase  16982  phlplusg  16983  phlsca  16984  phlvsca  16985  phlip  16986  odrngbas  17033  odrngplusg  17034  odrngmulr  17035  odrngtset  17036  odrngle  17037  odrngds  17038  prdsvallem  17082  prdsval  17083  prdssca  17084  prdsbas  17085  prdsplusg  17086  prdsmulr  17087  prdsvsca  17088  prdsip  17089  prdsle  17090  prdsds  17092  prdstset  17094  prdshom  17095  prdsco  17096  imasbas  17140  imasds  17141  imasplusg  17145  imasmulr  17146  imassca  17147  imasvsca  17148  imasip  17149  imastset  17150  imasle  17151  wunfunc  17530  wunfuncOLD  17531  fullfunc  17538  fthfunc  17539  isfull  17542  isfth  17546  wunnat  17588  wunnatOLD  17589  dmcoass  17697  catcisolem  17741  catciso  17742  catcoppccl  17748  catcoppcclOLD  17749  catcfuccl  17750  catcfucclOLD  17751  catcxpccl  17840  catcxpcclOLD  17841  ipobas  18164  ipolerval  18165  ipotset  18166  psdmrn  18206  psss  18213  ledm  18223  lern  18224  dirdm  18233  dirge  18236  mulgfval  18617  mvdco  18968  f1omvdconj  18969  gexex  19369  gsumval3  19423  lssacs  20144  cnfldbas  20514  cnfldadd  20515  cnfldmul  20516  cnfldcj  20517  cnfldtset  20518  cnfldle  20519  cnfldds  20520  cnfldunif  20521  rge0srg  20581  zntoslem  20676  asplss  20988  aspsubrg  20990  psrass1lemOLD  21053  psrass1lem  21056  psrbas  21057  psrplusg  21060  psrmulr  21063  psrsca  21068  psrvscafval  21069  psrass1  21084  psrass23l  21087  psrcom  21088  psrass23  21089  psropprmul  21319  coe1mul2  21350  ofco2  21508  toponsspwpw  21979  dmtopon  21980  leordtval2  22271  lmbrf  22319  lmres  22359  fiuncmp  22463  comppfsc  22591  1stckgenlem  22612  kgencn3  22617  ptbasfi  22640  xkoopn  22648  txcnmpt  22683  txkgen  22711  opnfbas  22901  fmfnfmlem4  23016  tsmsxplem1  23212  trust  23289  restutop  23297  nmoffn  23781  nmofval  23784  nmogelb  23786  nmolb  23787  nmof  23789  qtopbas  23829  tgqioo  23869  re2ndc  23870  iitopon  23948  dfii3  23952  iimulcn  24007  cnheiborlem  24023  bndth  24027  lebnumii  24035  reparphti  24066  pcoass  24093  cphsqrtcl  24253  lmmbrf  24331  iscauf  24349  caucfil  24352  lmclimf  24373  rrxmval  24474  rrxmet  24477  ovolfioo  24536  ovolficc  24537  ovolficcss  24538  ovolfsf  24540  ovollb  24548  ovolicc2lem3  24588  ovolicc2lem4  24589  ovolicc2  24591  volf  24598  volsup  24625  ovolfs2  24640  uniiccdif  24647  uniioovol  24648  uniiccvol  24649  uniioombllem2  24652  uniioombllem3a  24653  uniioombllem3  24654  uniioombllem4  24655  uniioombllem5  24656  uniioombl  24658  dyadmbllem  24668  dyadmbl  24669  opnmbllem  24670  opnmblALT  24672  volsup2  24674  vitalilem4  24680  vitalilem5  24681  vitali  24682  mbfimaopnlem  24724  mbflimsup  24735  i1f0  24756  i1f1  24759  itg11  24760  itg2mulc  24817  itg2gt0  24830  ellimc2  24946  limcresi  24954  dvreslem  24978  dvres2lem  24979  dvaddbr  25007  dvmulbr  25008  dvlipcn  25063  c1liplem1  25065  lhop1lem  25082  lhop1  25083  lhop2  25084  lhop  25085  dvfsumrlim  25100  ftc1cn  25112  itgsubstlem  25117  itgsubst  25118  itgpowd  25119  mdegleb  25134  mdeglt  25135  mdegldg  25136  mdegxrcl  25137  mdegcl  25139  mdegaddle  25144  mdegmullem  25148  deg1mul3le  25186  ig1peu  25241  ig1pdvds  25246  aacjcl  25392  aannenlem2  25394  aannenlem3  25395  aalioulem2  25398  taylfval  25423  radcnvcl  25481  radcnvlt1  25482  radcnvle  25484  abelth  25505  abelth2  25506  pilem2  25516  pilem3  25517  pige3ALT  25581  recosf1o  25596  resinf1o  25597  tanord1  25598  logcn  25707  dvlog  25711  dvlog2lem  25712  efopn  25718  logtayl  25720  cxpcn3  25806  loglesqrt  25816  ssscongptld  25877  leibpi  25997  efrlim  26024  jensenlem1  26041  jensenlem2  26042  jensen  26043  amgm  26045  lgamgulmlem2  26084  ftalem5  26131  efnnfsumcl  26157  efchtdvds  26213  dvdsmulf1o  26248  fsumdvdsmul  26249  lgsfcl2  26356  2sqlem6  26476  2sqlem8  26479  2sqlem9  26480  rpvmasumlem  26540  rpvmasum2  26565  dchrisum0re  26566  dchrisum0lem3  26572  dchrisum0  26573  rplogsum  26580  dirith2  26581  axtgcgrrflx  26727  axtgcgrid  26728  axtgsegcon  26729  axtg5seg  26730  axtgbtwnid  26731  axtgpasch  26732  axtgcont1  26733  tgcgr4  26796  motcgrg  26809  tglng  26811  upgrss  27361  pthdivtx  27998  disjxwwlkn  28179  ex-fpar  28727  nmlno0lem  29056  hlimcaui  29499  chsspwh  29510  shsss  29576  chintcli  29594  shsleji  29633  shub1i  29637  shsval2i  29650  lejdii  29801  spanuni  29807  sshhococi  29809  spansnpji  29841  osumcori  29906  5oai  29924  3oalem6  29930  3oai  29931  pjssmii  29944  mayete3i  29991  mayetes3i  29992  nmlnop0iALT  30258  imaelshi  30321  pjnmopi  30411  pjclem1  30458  pjci  30463  mdslmd1lem1  30588  shatomistici  30624  hatomistici  30625  chpssati  30626  xppreima  30884  iundisjfi  31019  iundisj2fi  31020  fprodex01  31041  xrsmulgzz  31189  fsumrp0cl  31206  gsummpt2co  31210  cycpmfv2  31283  cycpmrn  31312  xrge0slmod  31450  lsmsnorb  31481  idlsrgbas  31551  idlsrgplusg  31552  idlsrgmulr  31554  idlsrgtset  31555  ordtconnlem1  31776  xrge0iifhom  31789  lmlimxrge0  31800  lmxrge0  31804  indsumin  31890  esumcst  31931  esumpfinvallem  31942  esumpfinval  31943  esumpfinvalf  31944  esumcvg  31954  imambfm  32129  elmbfmvol2  32134  sxbrsigalem3  32139  sxbrsigalem2  32153  sxbrsigalem4  32154  sitgclg  32209  eulerpartlem1  32234  eulerpartlemgvv  32243  eulerpartlemgh  32245  eulerpartlemgf  32246  ballotlemfc0  32359  ballotlemfcc  32360  ballotlemiex  32368  ballotlemsup  32371  ballotlemsima  32382  ballotlemrv2  32388  ballotth  32404  signsplypnf  32429  signsply0  32430  rpsqrtcn  32473  itgexpif  32486  fsum2dsub  32487  reprfi2  32503  chtvalz  32509  breprexplemc  32512  breprexpnat  32514  circlemeth  32520  circlemethnat  32521  circlevma  32522  circlemethhgt  32523  hgt750lemd  32528  hgt750lema  32537  tgoldbachgtde  32540  tgoldbachgtda  32541  tgoldbachgt  32543  bnj1145  32873  bnj1286  32899  subfacp1lem2a  33042  erdszelem4  33056  erdszelem5  33057  erdszelem7  33059  erdszelem8  33060  kur14lem7  33074  kur14lem9  33076  cvxpconn  33104  cvxsconn  33105  resconn  33108  iccllysconn  33112  ttrclco  33704  cottrcl  33705  noextendseq  33797  oldf  33968  leftssno  33990  rightssno  33991  txpss3v  34107  txprel  34108  limitssson  34140  finminlem  34434  tailf  34491  filnetlem3  34496  onint1  34565  bj-unrab  35041  bj-2upln1upl  35141  bj-imdirco  35288  bj-rvecssabl  35404  taupilem2  35420  taupi  35421  poimirlem3  35707  poimirlem30  35734  poimirlem31  35735  poimirlem32  35736  broucube  35738  opnmbllem0  35740  mblfinlem1  35741  mblfinlem2  35742  mblfinlem3  35743  mblfinlem4  35744  ismblfin  35745  mbfposadd  35751  cnambfre  35752  itg2addnc  35758  ftc1cnnclem  35775  ftc1cnnc  35776  ftc1anclem3  35779  ftc1anclem7  35783  ftc1anc  35785  ftc2nc  35786  dvreasin  35790  dvreacos  35791  areacirclem1  35792  areacirclem2  35793  areacirc  35797  caures  35845  reheibor  35924  xrnss3v  36429  xrnrel  36430  atlatmstc  37260  atlatle  37261  pmaple  37702  sspadd1  37756  sspadd2  37757  dvrelog2  40000  dvrelog3  40001  diophin  40510  4rexfrabdioph  40536  6rexfrabdioph  40537  irrapxlem1  40560  irrapx1  40566  monotuz  40679  jm2.27dlem5  40751  hbtlem2  40865  algbase  40919  algaddg  40920  algmulr  40921  algsca  40922  algvsca  40923  arearect  40962  areaquad  40963  rtrclex  41114  trclubgNEW  41115  trclexi  41117  rtrclexi  41118  cnvtrcl0  41123  dfrtrcl5  41126  trrelsuperrel2dg  41168  relexpaddss  41215  brtrclfv2  41224  frege131d  41261  xphe  41278  clsk3nimkb  41539  gneispace  41633  k0004val0  41653  inaex  41804  lhe4.4ex1a  41836  uzmptshftfval  41853  binomcxplemdvbinom  41860  binomcxplemcvg  41861  binomcxplemnotnn0  41863  relopabVD  42410  fzisoeu  42729  fzsscn  42740  fzssre  42743  fzossuz  42810  zssxr  42827  uzssre2  42837  supminfxr  42894  uzsscn  42906  rpssxr  42911  uzinico  42988  limcresiooub  43073  limcresioolb  43074  limcleqr  43075  limclner  43082  limclr  43086  limsupequzmpt2  43149  liminfval2  43199  liminfequzmpt2  43222  icccncfext  43318  cncficcgt0  43319  ioodvbdlimc1lem2  43363  ioodvbdlimc2lem  43365  dvnprodlem1  43377  dvnprodlem2  43378  itgsin0pilem1  43381  itgsinexplem1  43385  itgsinexp  43386  dirkercncflem2  43535  fourierdlem16  43554  fourierdlem18  43556  fourierdlem20  43558  fourierdlem21  43559  fourierdlem22  43560  fourierdlem25  43563  fourierdlem37  43575  fourierdlem42  43580  fourierdlem50  43587  fourierdlem52  43589  fourierdlem62  43599  fourierdlem64  43601  fourierdlem66  43603  fourierdlem68  43605  fourierdlem74  43611  fourierdlem75  43612  fourierdlem76  43613  fourierdlem79  43616  fourierdlem83  43620  fourierdlem95  43632  fourierdlem101  43638  fourierdlem102  43639  fourierdlem103  43640  fourierdlem104  43641  fourierdlem112  43649  fourierdlem114  43651  sqwvfoura  43659  sqwvfourb  43660  fouriersw  43662  etransclem24  43689  etransclem48  43713  sge0sn  43807  sge0tsms  43808  sge0f1o  43810  sge0pr  43822  sge0resplit  43834  sge0split  43837  sge0iunmptlemre  43843  sge0isummpt2  43860  carageniuncllem1  43949  hoicvr  43976  hoicvrrex  43984  hoidmvlelem2  44024  hspmbl  44057  smfmullem4  44215  prmdvdsfmtnof1lem1  44924  prmdvdsfmtnof  44926  oddibas  45255  2zrngbas  45382  2zrng0  45384  sepfsepc  46109  aacllem  46391  amgmlemALT  46393