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  6835  ssimaex  6963  riotassuni  7410  oprabss  7521  dmexg  7898  rnexg  7899  mptmpoopabbrd  8080  fparlem3  8111  fparlem4  8112  snopsuppss  8177  tposssxp  8228  naddunif  8682  naddasslem1  8683  naddasslem2  8684  mapsspw  8885  sbthlem5  9089  sbthlem7  9091  cnvimamptfin  9320  marypha1lem  9403  ordtypelem4  9493  hartogslem1  9514  ttrclco  9697  cottrcl  9698  tc2  9719  frmin  9731  frrlem16  9740  tz9.12lem1  9769  rankval4  9849  rankxpl  9857  rankmapu  9860  rankxplim  9861  djuin  9923  infxpenlem  10016  ackbij1lem18  10238  cflm  10251  fin23lem29  10343  hsmexlem4  10431  hsmexlem5  10432  brdom3  10531  brdom5  10532  brdom4  10533  smobeth  10595  pwfseqlem3  10669  wundm  10737  wunrn  10738  wunex2  10747  ltsopi  10897  dmaddpi  10899  dmmulpi  10900  nqerf  10939  ltrelxr  11294  uzssre  12909  uzwo2  12961  infssuzle  12980  infssuzcl  12981  uzwo3  12992  nn0ssq  13006  nnssq  13007  qsscn  13009  rpnnen1lem3  13029  rpnnen1lem5  13031  dflt2  13199  ioosscn  13461  unitsscn  13553  fzval2  13564  fzossz  13735  fzossnn  13767  injresinj  13847  flval3  13876  uzsup  13924  uzrdgfni  14022  expcl2lem  14137  rpexpcl  14144  expge0  14162  expge1  14163  hashxrcl  14421  seqcoll  14529  xptrrel  15053  trclublem  15068  01sqrexlem3  15331  limsupval2  15567  limsupgre  15568  rlimpm  15587  rlimclim  15633  isercolllem1  15752  isercolllem2  15753  isercoll  15755  caurcvg  15764  caucvg  15766  summolem2a  15801  summolem2  15802  zsum  15804  fsumcvg3  15815  fsumrpcl  15823  fsumge0  15882  climfsum  15907  ackbijnn  15917  prodmolem2a  16021  prodmolem2  16022  zprod  16024  fprodrpcl  16043  fprodge0  16080  fprodge1  16082  rprisefaccl  16110  divalglem8  16490  sadaddlem  16556  lcmfval  16711  isprm3  16773  maxprmfct  16800  pclem  16930  prmreclem1  17008  prmreclem2  17009  prmreclem3  17010  1arith  17019  4sqlem11  17047  ramtlecl  17092  ramcl2lem  17101  ramxrcl  17109  prmgaplem3  17145  prmgaplem4  17146  cshwshashlem1  17187  structfn  17248  strleun  17249  ressbasss  17331  ressbasss2  17333  srngbase  17395  srngplusg  17396  srngmulr  17397  lmodbase  17411  lmodplusg  17412  lmodsca  17413  ipsbase  17422  ipsaddg  17423  ipsmulr  17424  ipssca  17425  ipsvsca  17426  ipsip  17427  phlbase  17432  phlplusg  17433  phlsca  17434  phlvsca  17435  phlip  17436  odrngbas  17489  odrngplusg  17490  odrngmulr  17491  odrngtset  17492  odrngle  17493  odrngds  17494  prdsvallem  17539  prdsval  17540  prdssca  17541  prdsbas  17542  prdsplusg  17543  prdsmulr  17544  prdsvsca  17545  prdsip  17546  prdsle  17547  prdsds  17549  prdstset  17551  prdshom  17552  prdsco  17553  imasbas  17598  imasds  17599  imasplusg  17603  imasmulr  17604  imassca  17605  imasvsca  17606  imasip  17607  imastset  17608  imasle  17609  wunfunc  17990  fullfunc  17997  fthfunc  17998  isfull  18001  isfth  18005  wunnat  18048  dmcoass  18155  catcisolem  18199  catciso  18200  catcoppccl  18206  catcfuccl  18207  catcxpccl  18295  ipobas  18619  ipolerval  18620  ipotset  18621  psdmrn  18661  psss  18668  ledm  18678  lern  18679  dirdm  18688  dirge  18691  mulgfval  19192  mvdco  19572  f1omvdconj  19573  gexex  19980  gsumval3  20034  lssacs  21151  cnfldbas  21589  mpocnfldadd  21590  mpocnfldmul  21592  cnfldcj  21594  cnfldtset  21595  cnfldle  21596  cnfldds  21597  cnfldunif  21598  rge0srg  21651  zntoslem  21769  asplss  22088  aspsubrg  22090  psrass1lem  22148  psrbas  22149  psrplusg  22152  psrmulr  22157  psrsca  22162  psrvscafval  22163  psrass1  22178  psrass23l  22181  psrcom  22182  psrass23  22183  psropprmul  22462  coe1mul2  22495  ofco2  22673  toponsspwpw  23147  dmtopon  23148  leordtval2  23437  lmbrf  23485  lmres  23525  fiuncmp  23629  comppfsc  23758  1stckgenlem  23779  kgencn3  23784  ptbasfi  23807  xkoopn  23815  txcnmpt  23850  txkgen  23878  opnfbas  24068  fmfnfmlem4  24183  tsmsxplem1  24379  trust  24455  restutop  24463  nmoffn  24937  nmofval  24940  nmogelb  24942  nmolb  24943  nmof  24945  qtopbas  24985  tgqioo  25026  re2ndc  25027  iitopon  25107  dfii3  25111  cnheiborlem  25182  bndth  25186  lebnumii  25194  pcoass  25252  cphsqrtcl  25412  lmmbrf  25490  iscauf  25508  caucfil  25511  lmclimf  25532  rrxmval  25633  rrxmet  25636  ovolfioo  25695  ovolficc  25696  ovolficcss  25697  ovolfsf  25699  ovollb  25707  ovolicc2lem3  25747  ovolicc2lem4  25748  ovolicc2  25750  volf  25757  volsup  25784  ovolfs2  25799  uniiccdif  25806  uniioovol  25807  uniiccvol  25808  uniioombllem2  25811  uniioombllem3a  25812  uniioombllem3  25813  uniioombllem4  25814  uniioombllem5  25815  uniioombl  25817  dyadmbllem  25827  dyadmbl  25828  opnmbllem  25829  opnmblALT  25831  volsup2  25833  vitalilem4  25839  vitalilem5  25840  vitali  25841  mbfimaopnlem  25883  mbflimsup  25894  i1f0  25915  i1f1  25918  itg11  25919  itg2mulc  25975  itg2gt0  25988  ellimc2  26104  limcresi  26112  dvreslem  26136  dvres2lem  26137  dvaddbr  26165  dvmulbr  26166  dvlipcn  26221  c1liplem1  26223  lhop1lem  26240  lhop1  26241  lhop2  26242  lhop  26243  dvfsumrlim  26258  ftc1cn  26270  itgsubstlem  26275  itgsubst  26276  itgpowd  26277  mdegleb  26289  mdeglt  26290  mdegldg  26291  mdegxrcl  26292  mdegcl  26294  mdegaddle  26299  mdegmullem  26303  deg1mul3le  26342  ig1peu  26400  ig1pdvds  26405  aacjcl  26563  aannenlem2  26565  aannenlem3  26566  aalioulem2  26569  taylfval  26595  radcnvcl  26653  radcnvlt1  26654  radcnvle  26656  abelth  26677  abelth2  26678  pilem2  26688  pilem3  26689  pige3ALT  26757  recosf1o  26772  resinf1o  26773  tanord1  26774  logcn  26884  dvlog  26888  dvlog2lem  26889  efopn  26895  logtayl  26897  cxpcn3  26985  loglesqrt  26998  ssscongptld  27059  leibpi  27179  efrlim  27206  jensenlem1  27223  jensenlem2  27224  jensen  27225  amgm  27227  lgamgulmlem2  27266  ftalem5  27313  efnnfsumcl  27339  efchtdvds  27395  mpodvdsmulf1o  27430  fsumdvdsmul  27431  dvdsmulf1o  27432  lgsfcl2  27539  2sqlem6  27659  2sqlem8  27662  2sqlem9  27663  rpvmasumlem  27723  rpvmasum2  27748  dchrisum0re  27749  dchrisum0lem3  27755  dchrisum0  27756  rplogsum  27763  dirith2  27764  noextendseq  27903  oldf  28102  leftssno  28138  rightssno  28139  addbdaylem  28282  mulsproplem12  28392  mulsproplem13  28393  mulsproplem14  28394  mulsasslem3  28430  precsexlem11  28482  oncutlt  28529  bdayons  28541  nnssno  28587  axtgcgrrflx  28803  axtgcgrid  28804  axtgsegcon  28805  axtg5seg  28806  axtgbtwnid  28807  axtgpasch  28808  axtgcont1  28809  tgcgr4  28873  motcgrg  28886  tglng  28888  upgrss  29545  pthdivtx  30191  disjxwwlkn  30381  ex-fpar  30942  nmlno0lem  31274  hlimcaui  31717  chsspwh  31728  shsss  31794  chintcli  31812  shsleji  31851  shub1i  31855  shsval2i  31868  lejdii  32019  spanuni  32025  sshhococi  32027  spansnpji  32059  osumcori  32124  5oai  32142  3oalem6  32148  3oai  32149  pjssmii  32162  mayete3i  32209  mayetes3i  32210  nmlnop0iALT  32476  imaelshi  32539  pjnmopi  32629  pjclem1  32676  pjci  32681  mdslmd1lem1  32806  shatomistici  32842  hatomistici  32843  chpssati  32844  xppreima  33118  iundisjfi  33267  iundisj2fi  33268  fprodex01  33295  indsumin  33307  xrsmulgzz  33449  fsumrp0cl  33461  gsummpt2co  33488  cycpmfv2  33554  cycpmrn  33583  rlocbas  33708  rlocaddval  33709  rlocmulval  33710  1fldgenq  33763  xrge0slmod  33788  lsmsnorb  33824  idlsrgbas  33914  idlsrgplusg  33915  idlsrgmulr  33917  idlsrgtset  33918  selvply1rhmlemb  34029  esplyind  34085  vietalem  34089  constrextdg2  34259  ordtconnlem1  34434  xrge0iifhom  34447  lmlimxrge0  34458  lmxrge0  34462  esumcst  34573  esumpfinvallem  34584  esumpfinval  34585  esumpfinvalf  34586  esumcvg  34596  imambfm  34773  elmbfmvol2  34778  sxbrsigalem3  34783  sxbrsigalem2  34797  sxbrsigalem4  34798  sitgclg  34853  eulerpartlem1  34878  eulerpartlemgvv  34887  eulerpartlemgh  34889  eulerpartlemgf  34890  ballotlemfc0  35004  ballotlemfcc  35005  ballotlemiex  35013  ballotlemsup  35016  ballotlemsima  35027  ballotlemrv2  35033  ballotth  35049  signsplypnf  35058  signsply0  35059  rpsqrtcn  35101  itgexpif  35114  fsum2dsub  35115  reprfi2  35131  chtvalz  35137  breprexplemc  35140  breprexpnat  35142  circlemeth  35148  circlemethnat  35149  circlevma  35150  circlemethhgt  35151  hgt750lemd  35156  hgt750lema  35165  tgoldbachgtde  35168  tgoldbachgtda  35169  tgoldbachgt  35171  bnj1145  35502  bnj1286  35528  subfacp1lem2a  35759  erdszelem4  35773  erdszelem5  35774  erdszelem7  35776  erdszelem8  35777  kur14lem7  35791  kur14lem9  35793  resconn  35825  iccllysconn  35829  txpss3v  36455  txprel  36456  limitssson  36488  finminlem  36937  tailf  36994  filnetlem3  36999  onint1  37068  ttcuniun  37129  bj-unrab  37670  bj-2upln1upl  37768  bj-imdirco  37942  bj-rvecssabl  38058  taupilem2  38074  taupi  38075  poimirlem3  38372  poimirlem30  38399  poimirlem31  38400  poimirlem32  38401  broucube  38403  opnmbllem0  38405  mblfinlem1  38406  mblfinlem2  38407  mblfinlem3  38408  mblfinlem4  38409  ismblfin  38410  mbfposadd  38416  cnambfre  38417  itg2addnc  38423  ftc1cnnclem  38440  ftc1cnnc  38441  ftc1anclem3  38444  ftc1anclem7  38448  ftc1anc  38450  ftc2nc  38451  dvreasin  38455  dvreacos  38456  areacirclem1  38457  areacirclem2  38458  areacirc  38462  caures  38510  reheibor  38589  xrnss3v  39129  xrnrel  39130  atlatmstc  40192  atlatle  40193  pmaple  40634  sspadd1  40688  sspadd2  40689  dvrelog2  42930  dvrelog3  42931  rpsscn  43174  sumcubes  43188  redvmptabs  43235  diophin  43617  4rexfrabdioph  43639  6rexfrabdioph  43640  irrapxlem1  43663  irrapx1  43669  rmxyelqirr  43751  monotuz  43782  jm2.27dlem5  43854  hbtlem2  43965  algbase  44015  algaddg  44016  algmulr  44017  algsca  44018  algvsca  44019  arearect  44056  areaquad  44057  rtrclex  44457  trclubgNEW  44458  trclexi  44460  rtrclexi  44461  cnvtrcl0  44466  dfrtrcl5  44469  trrelsuperrel2dg  44511  relexpaddss  44558  brtrclfv2  44567  frege131d  44604  xphe  44621  clsk3nimkb  44880  gneispace  44974  k0004val0  44994  inaex  45121  lhe4.4ex1a  45153  uzmptshftfval  45170  binomcxplemdvbinom  45177  binomcxplemcvg  45178  binomcxplemnotnn0  45180  relopabVD  45723  dmwf  45788  rnwf  45789  fzisoeu  46133  fzsscn  46144  fzssre  46147  fzossuz  46210  zssxr  46226  uzssre2  46235  supminfxr  46292  uzsscn  46303  rpssxr  46308  uzinico  46389  limcresiooub  46470  limcresioolb  46471  limcleqr  46472  limclner  46479  limclr  46483  limsupequzmpt2  46546  liminfval2  46596  liminfequzmpt2  46619  icccncfext  46715  cncficcgt0  46716  ioodvbdlimc1lem2  46760  ioodvbdlimc2lem  46762  dvnprodlem2  46775  itgsin0pilem1  46778  itgsinexplem1  46782  itgsinexp  46783  dirkercncflem2  46932  fourierdlem16  46951  fourierdlem18  46953  fourierdlem20  46955  fourierdlem21  46956  fourierdlem22  46957  fourierdlem25  46960  fourierdlem37  46972  fourierdlem42  46977  fourierdlem50  46984  fourierdlem52  46986  fourierdlem62  46996  fourierdlem64  46998  fourierdlem66  47000  fourierdlem68  47002  fourierdlem74  47008  fourierdlem75  47009  fourierdlem76  47010  fourierdlem79  47013  fourierdlem83  47017  fourierdlem95  47029  fourierdlem101  47035  fourierdlem102  47036  fourierdlem103  47037  fourierdlem104  47038  fourierdlem112  47046  fourierdlem114  47048  sqwvfoura  47056  sqwvfourb  47057  fouriersw  47059  etransclem24  47086  etransclem48  47110  sge0sn  47207  sge0tsms  47208  sge0f1o  47210  sge0pr  47222  sge0resplit  47234  sge0split  47237  sge0iunmptlemre  47243  sge0isummpt2  47260  carageniuncllem1  47349  hoicvr  47376  hoicvrrex  47384  hoidmvlelem2  47424  hspmbl  47457  smfmullem4  47622  chnsuslle  47709  lamberte  47756  rehalfge1  48227  prmdvdsfmtnof1lem1  48487  prmdvdsfmtnof  48489  upgrimpthslem2  48824  upgrimpths  48825  oddibas  49088  2zrngbas  49157  2zrng0  49159  dmtposss  49802  tposres3  49807  sepfsepc  49854  uptrlem1  50136  uptrlem2  50137  uptrlem3  50138  uptra  50141  uptrar  50142  uobeqw  50145  uptr2  50147  uptr2a  50148  fucoppcfunc  50338  aacllem  50772  amgmlemALT  50821