Theorem sstri 3991

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

Syntax hints:   ⊆ wss 3948

This theorem was proved from axioms:  ax-mp 5  ax-1 6  ax-2 7  ax-3 8  ax-gen 1798  ax-4 1812  ax-5 1914  ax-6 1972  ax-7 2012  ax-8 2109  ax-9 2117  ax-ext 2704

This theorem depends on definitions:  df-bi 206  df-an 398  df-tru 1545  df-ex 1783  df-sb 2069  df-clab 2711  df-cleq 2725  df-clel 2811  df-v 3477  df-in 3955  df-ss 3965

This theorem is referenced by:  snsstp1  4819  snsstp2  4820  uniintsn  4991  elopabran  5562  ssrnres  6175  cossxp  6269  foimacnv  6848  ssimaex  6974  riotassuni  7403  oprabss  7512  dmexg  7891  rnexg  7892  fabexg  7922  fparlem3  8097  fparlem4  8098  snopsuppss  8161  tposssxp  8212  naddunif  8689  naddasslem1  8690  naddasslem2  8691  mapsspw  8869  sbthlem5  9084  sbthlem7  9086  cnvimamptfin  9350  marypha1lem  9425  ordtypelem4  9513  hartogslem1  9534  ttrclco  9710  cottrcl  9711  tc2  9734  frmin  9741  frrlem16  9750  tz9.12lem1  9779  rankval4  9859  rankxpl  9867  rankmapu  9870  rankxplim  9871  djuin  9910  infxpenlem  10005  ackbij1lem18  10229  cflm  10242  fin23lem29  10333  hsmexlem4  10421  hsmexlem5  10422  brdom3  10520  brdom5  10521  brdom4  10522  smobeth  10578  pwfseqlem3  10652  wundm  10720  wunrn  10721  wunex2  10730  ltsopi  10880  dmaddpi  10882  dmmulpi  10883  nqerf  10922  ltrelxr  11272  uzssre  12841  uzwo2  12893  infssuzle  12912  infssuzcl  12913  uzwo3  12924  nn0ssq  12938  nnssq  12939  qsscn  12941  rpnnen1lem3  12960  rpnnen1lem5  12962  dflt2  13124  ioosscn  13383  unitsscn  13474  fzval2  13484  fzossz  13649  fzossnn  13678  injresinj  13750  flval3  13777  uzsup  13825  uzrdgfni  13920  expcl2lem  14036  rpexpcl  14043  expge0  14061  expge1  14062  hashxrcl  14314  seqcoll  14422  xptrrel  14924  trclublem  14939  01sqrexlem3  15188  limsupval2  15421  limsupgre  15422  rlimpm  15441  rlimclim  15487  isercolllem1  15608  isercolllem2  15609  isercoll  15611  caurcvg  15620  caucvg  15622  summolem2a  15658  summolem2  15659  zsum  15661  fsumcvg3  15672  fsumrpcl  15680  fsumge0  15738  climfsum  15763  ackbijnn  15771  prodmolem2a  15875  prodmolem2  15876  zprod  15878  fprodrpcl  15897  fprodge0  15934  fprodge1  15936  rprisefaccl  15964  divalglem8  16340  sadaddlem  16404  lcmfval  16555  isprm3  16617  maxprmfct  16643  pclem  16768  prmreclem1  16846  prmreclem2  16847  prmreclem3  16848  1arith  16857  4sqlem11  16885  ramtlecl  16930  ramcl2lem  16939  ramxrcl  16947  prmgaplem3  16983  prmgaplem4  16984  cshwshashlem1  17026  structfn  17086  strleun  17087  ressbasss  17180  ressbasss2  17182  srngbase  17252  srngplusg  17253  srngmulr  17254  lmodbase  17268  lmodplusg  17269  lmodsca  17270  ipsbase  17279  ipsaddg  17280  ipsmulr  17281  ipssca  17282  ipsvsca  17283  ipsip  17284  phlbase  17289  phlplusg  17290  phlsca  17291  phlvsca  17292  phlip  17293  odrngbas  17346  odrngplusg  17347  odrngmulr  17348  odrngtset  17349  odrngle  17350  odrngds  17351  prdsvallem  17397  prdsval  17398  prdssca  17399  prdsbas  17400  prdsplusg  17401  prdsmulr  17402  prdsvsca  17403  prdsip  17404  prdsle  17405  prdsds  17407  prdstset  17409  prdshom  17410  prdsco  17411  imasbas  17455  imasds  17456  imasplusg  17460  imasmulr  17461  imassca  17462  imasvsca  17463  imasip  17464  imastset  17465  imasle  17466  wunfunc  17846  wunfuncOLD  17847  fullfunc  17854  fthfunc  17855  isfull  17858  isfth  17862  wunnat  17904  wunnatOLD  17905  dmcoass  18013  catcisolem  18057  catciso  18058  catcoppccl  18064  catcoppcclOLD  18065  catcfuccl  18066  catcfucclOLD  18067  catcxpccl  18156  catcxpcclOLD  18157  ipobas  18481  ipolerval  18482  ipotset  18483  psdmrn  18523  psss  18530  ledm  18540  lern  18541  dirdm  18550  dirge  18553  mulgfval  18947  mvdco  19308  f1omvdconj  19309  gexex  19716  gsumval3  19770  lssacs  20571  cnfldbas  20941  cnfldadd  20942  cnfldmul  20943  cnfldcj  20944  cnfldtset  20945  cnfldle  20946  cnfldds  20947  cnfldunif  20948  rge0srg  21009  zntoslem  21104  asplss  21420  aspsubrg  21422  psrass1lemOLD  21485  psrass1lem  21488  psrbas  21489  psrplusg  21492  psrmulr  21495  psrsca  21500  psrvscafval  21501  psrass1  21517  psrass23l  21520  psrcom  21521  psrass23  21522  psropprmul  21752  coe1mul2  21783  ofco2  21945  toponsspwpw  22416  dmtopon  22417  leordtval2  22708  lmbrf  22756  lmres  22796  fiuncmp  22900  comppfsc  23028  1stckgenlem  23049  kgencn3  23054  ptbasfi  23077  xkoopn  23085  txcnmpt  23120  txkgen  23148  opnfbas  23338  fmfnfmlem4  23453  tsmsxplem1  23649  trust  23726  restutop  23734  nmoffn  24220  nmofval  24223  nmogelb  24225  nmolb  24226  nmof  24228  qtopbas  24268  tgqioo  24308  re2ndc  24309  iitopon  24387  dfii3  24391  iimulcn  24446  cnheiborlem  24462  bndth  24466  lebnumii  24474  reparphti  24505  pcoass  24532  cphsqrtcl  24693  lmmbrf  24771  iscauf  24789  caucfil  24792  lmclimf  24813  rrxmval  24914  rrxmet  24917  ovolfioo  24976  ovolficc  24977  ovolficcss  24978  ovolfsf  24980  ovollb  24988  ovolicc2lem3  25028  ovolicc2lem4  25029  ovolicc2  25031  volf  25038  volsup  25065  ovolfs2  25080  uniiccdif  25087  uniioovol  25088  uniiccvol  25089  uniioombllem2  25092  uniioombllem3a  25093  uniioombllem3  25094  uniioombllem4  25095  uniioombllem5  25096  uniioombl  25098  dyadmbllem  25108  dyadmbl  25109  opnmbllem  25110  opnmblALT  25112  volsup2  25114  vitalilem4  25120  vitalilem5  25121  vitali  25122  mbfimaopnlem  25164  mbflimsup  25175  i1f0  25196  i1f1  25199  itg11  25200  itg2mulc  25257  itg2gt0  25270  ellimc2  25386  limcresi  25394  dvreslem  25418  dvres2lem  25419  dvaddbr  25447  dvmulbr  25448  dvlipcn  25503  c1liplem1  25505  lhop1lem  25522  lhop1  25523  lhop2  25524  lhop  25525  dvfsumrlim  25540  ftc1cn  25552  itgsubstlem  25557  itgsubst  25558  itgpowd  25559  mdegleb  25574  mdeglt  25575  mdegldg  25576  mdegxrcl  25577  mdegcl  25579  mdegaddle  25584  mdegmullem  25588  deg1mul3le  25626  ig1peu  25681  ig1pdvds  25686  aacjcl  25832  aannenlem2  25834  aannenlem3  25835  aalioulem2  25838  taylfval  25863  radcnvcl  25921  radcnvlt1  25922  radcnvle  25924  abelth  25945  abelth2  25946  pilem2  25956  pilem3  25957  pige3ALT  26021  recosf1o  26036  resinf1o  26037  tanord1  26038  logcn  26147  dvlog  26151  dvlog2lem  26152  efopn  26158  logtayl  26160  cxpcn3  26246  loglesqrt  26256  ssscongptld  26317  leibpi  26437  efrlim  26464  jensenlem1  26481  jensenlem2  26482  jensen  26483  amgm  26485  lgamgulmlem2  26524  ftalem5  26571  efnnfsumcl  26597  efchtdvds  26653  dvdsmulf1o  26688  fsumdvdsmul  26689  lgsfcl2  26796  2sqlem6  26916  2sqlem8  26919  2sqlem9  26920  rpvmasumlem  26980  rpvmasum2  27005  dchrisum0re  27006  dchrisum0lem3  27012  dchrisum0  27013  rplogsum  27020  dirith2  27021  noextendseq  27160  oldf  27342  leftssno  27365  rightssno  27366  mulsproplem12  27573  mulsproplem13  27574  mulsproplem14  27575  mulsasslem3  27610  precsexlem11  27653  axtgcgrrflx  27703  axtgcgrid  27704  axtgsegcon  27705  axtg5seg  27706  axtgbtwnid  27707  axtgpasch  27708  axtgcont1  27709  tgcgr4  27772  motcgrg  27785  tglng  27787  upgrss  28338  pthdivtx  28976  disjxwwlkn  29157  ex-fpar  29705  nmlno0lem  30034  hlimcaui  30477  chsspwh  30488  shsss  30554  chintcli  30572  shsleji  30611  shub1i  30615  shsval2i  30628  lejdii  30779  spanuni  30785  sshhococi  30787  spansnpji  30819  osumcori  30884  5oai  30902  3oalem6  30908  3oai  30909  pjssmii  30922  mayete3i  30969  mayetes3i  30970  nmlnop0iALT  31236  imaelshi  31299  pjnmopi  31389  pjclem1  31436  pjci  31441  mdslmd1lem1  31566  shatomistici  31602  hatomistici  31603  chpssati  31604  xppreima  31859  iundisjfi  31995  iundisj2fi  31996  fprodex01  32019  xrsmulgzz  32167  fsumrp0cl  32184  gsummpt2co  32188  cycpmfv2  32261  cycpmrn  32290  1fldgenq  32401  xrge0slmod  32452  lsmsnorb  32490  idlsrgbas  32607  idlsrgplusg  32608  idlsrgmulr  32610  idlsrgtset  32611  ordtconnlem1  32893  xrge0iifhom  32906  lmlimxrge0  32917  lmxrge0  32921  indsumin  33009  esumcst  33050  esumpfinvallem  33061  esumpfinval  33062  esumpfinvalf  33063  esumcvg  33073  imambfm  33250  elmbfmvol2  33255  sxbrsigalem3  33260  sxbrsigalem2  33274  sxbrsigalem4  33275  sitgclg  33330  eulerpartlem1  33355  eulerpartlemgvv  33364  eulerpartlemgh  33366  eulerpartlemgf  33367  ballotlemfc0  33480  ballotlemfcc  33481  ballotlemiex  33489  ballotlemsup  33492  ballotlemsima  33503  ballotlemrv2  33509  ballotth  33525  signsplypnf  33550  signsply0  33551  rpsqrtcn  33594  itgexpif  33607  fsum2dsub  33608  reprfi2  33624  chtvalz  33630  breprexplemc  33633  breprexpnat  33635  circlemeth  33641  circlemethnat  33642  circlevma  33643  circlemethhgt  33644  hgt750lemd  33649  hgt750lema  33658  tgoldbachgtde  33661  tgoldbachgtda  33662  tgoldbachgt  33664  bnj1145  33993  bnj1286  34019  subfacp1lem2a  34160  erdszelem4  34174  erdszelem5  34175  erdszelem7  34177  erdszelem8  34178  kur14lem7  34192  kur14lem9  34194  cvxpconn  34222  cvxsconn  34223  resconn  34226  iccllysconn  34230  txpss3v  34839  txprel  34840  limitssson  34872  gg-dvmulbr  35164  finminlem  35192  tailf  35249  filnetlem3  35254  onint1  35323  bj-unrab  35795  bj-2upln1upl  35894  bj-imdirco  36060  bj-rvecssabl  36176  taupilem2  36192  taupi  36193  poimirlem3  36480  poimirlem30  36507  poimirlem31  36508  poimirlem32  36509  broucube  36511  opnmbllem0  36513  mblfinlem1  36514  mblfinlem2  36515  mblfinlem3  36516  mblfinlem4  36517  ismblfin  36518  mbfposadd  36524  cnambfre  36525  itg2addnc  36531  ftc1cnnclem  36548  ftc1cnnc  36549  ftc1anclem3  36552  ftc1anclem7  36556  ftc1anc  36558  ftc2nc  36559  dvreasin  36563  dvreacos  36564  areacirclem1  36565  areacirclem2  36566  areacirc  36570  caures  36617  reheibor  36696  xrnss3v  37231  xrnrel  37232  atlatmstc  38178  atlatle  38179  pmaple  38621  sspadd1  38675  sspadd2  38676  dvrelog2  40918  dvrelog3  40919  sumcubes  41207  diophin  41496  4rexfrabdioph  41522  6rexfrabdioph  41523  irrapxlem1  41546  irrapx1  41552  rmxyelqirr  41634  monotuz  41666  jm2.27dlem5  41738  hbtlem2  41852  algbase  41906  algaddg  41907  algmulr  41908  algsca  41909  algvsca  41910  arearect  41950  areaquad  41951  rtrclex  42354  trclubgNEW  42355  trclexi  42357  rtrclexi  42358  cnvtrcl0  42363  dfrtrcl5  42366  trrelsuperrel2dg  42408  relexpaddss  42455  brtrclfv2  42464  frege131d  42501  xphe  42518  clsk3nimkb  42777  gneispace  42871  k0004val0  42891  inaex  43042  lhe4.4ex1a  43074  uzmptshftfval  43091  binomcxplemdvbinom  43098  binomcxplemcvg  43099  binomcxplemnotnn0  43101  relopabVD  43648  fzisoeu  43997  fzsscn  44008  fzssre  44011  fzossuz  44078  zssxr  44094  uzssre2  44104  supminfxr  44161  uzsscn  44173  rpssxr  44178  uzinico  44260  limcresiooub  44345  limcresioolb  44346  limcleqr  44347  limclner  44354  limclr  44358  limsupequzmpt2  44421  liminfval2  44471  liminfequzmpt2  44494  icccncfext  44590  cncficcgt0  44591  ioodvbdlimc1lem2  44635  ioodvbdlimc2lem  44637  dvnprodlem1  44649  dvnprodlem2  44650  itgsin0pilem1  44653  itgsinexplem1  44657  itgsinexp  44658  dirkercncflem2  44807  fourierdlem16  44826  fourierdlem18  44828  fourierdlem20  44830  fourierdlem21  44831  fourierdlem22  44832  fourierdlem25  44835  fourierdlem37  44847  fourierdlem42  44852  fourierdlem50  44859  fourierdlem52  44861  fourierdlem62  44871  fourierdlem64  44873  fourierdlem66  44875  fourierdlem68  44877  fourierdlem74  44883  fourierdlem75  44884  fourierdlem76  44885  fourierdlem79  44888  fourierdlem83  44892  fourierdlem95  44904  fourierdlem101  44910  fourierdlem102  44911  fourierdlem103  44912  fourierdlem104  44913  fourierdlem112  44921  fourierdlem114  44923  sqwvfoura  44931  sqwvfourb  44932  fouriersw  44934  etransclem24  44961  etransclem48  44985  sge0sn  45082  sge0tsms  45083  sge0f1o  45085  sge0pr  45097  sge0resplit  45109  sge0split  45112  sge0iunmptlemre  45118  sge0isummpt2  45135  carageniuncllem1  45224  hoicvr  45251  hoicvrrex  45259  hoidmvlelem2  45299  hspmbl  45332  smfmullem4  45497  prmdvdsfmtnof1lem1  46239  prmdvdsfmtnof  46241  oddibas  46570  2zrngbas  46788  2zrng0  46790  sepfsepc  47514  aacllem  47802  amgmlemALT  47804