Theorem sstri 3896

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

Syntax hints:   ⊆ wss 3853

This theorem was proved from axioms:  ax-mp 5  ax-1 6  ax-2 7  ax-3 8  ax-gen 1803  ax-4 1817  ax-5 1918  ax-6 1976  ax-7 2018  ax-8 2114  ax-9 2122  ax-ext 2708

This theorem depends on definitions:  df-bi 210  df-an 400  df-tru 1546  df-ex 1788  df-sb 2073  df-clab 2715  df-cleq 2728  df-clel 2809  df-v 3400  df-in 3860  df-ss 3870

This theorem is referenced by:  snsstp1  4715  snsstp2  4716  uniintsn  4884  ssrnres  6021  cossxp  6115  foimacnv  6656  ssimaex  6774  riotassuni  7189  oprabss  7295  dmexg  7659  rnexg  7660  fabexg  7690  fparlem3  7860  fparlem4  7861  snopsuppss  7899  tposssxp  7950  mapsspw  8537  sbthlem5  8738  sbthlem7  8740  cnvimamptfin  8955  marypha1lem  9027  ordtypelem4  9115  hartogslem1  9136  tc2  9336  tz9.12lem1  9368  rankval4  9448  rankxpl  9456  rankmapu  9459  rankxplim  9460  djuin  9499  infxpenlem  9592  ackbij1lem18  9816  cflm  9829  fin23lem29  9920  hsmexlem4  10008  hsmexlem5  10009  brdom3  10107  brdom5  10108  brdom4  10109  smobeth  10165  pwfseqlem3  10239  wundm  10307  wunrn  10308  wunex2  10317  ltsopi  10467  dmaddpi  10469  dmmulpi  10470  nqerf  10509  ltrelxr  10859  uzssre  12425  uzwo2  12473  infssuzle  12492  infssuzcl  12493  uzwo3  12504  nn0ssq  12518  nnssq  12519  qsscn  12521  rpnnen1lem3  12540  rpnnen1lem5  12542  dflt2  12703  ioosscn  12962  unitsscn  13053  fzval2  13063  fzossz  13227  fzossnn  13256  injresinj  13328  flval3  13355  uzsup  13401  uzrdgfni  13496  expcl2lem  13612  rpexpcl  13619  expge0  13636  expge1  13637  hashxrcl  13889  seqcoll  13995  xptrrel  14508  trclublem  14523  sqrlem3  14773  limsupval2  15006  limsupgre  15007  rlimpm  15026  rlimclim  15072  isercolllem1  15193  isercolllem2  15194  isercoll  15196  caurcvg  15205  caucvg  15207  summolem2a  15244  summolem2  15245  zsum  15247  fsumcvg3  15258  fsumrpcl  15266  fsumge0  15322  climfsum  15347  ackbijnn  15355  prodmolem2a  15459  prodmolem2  15460  zprod  15462  fprodrpcl  15481  fprodge0  15518  fprodge1  15520  rprisefaccl  15548  divalglem8  15924  sadaddlem  15988  lcmfval  16141  isprm3  16203  maxprmfct  16229  pclem  16354  prmreclem1  16432  prmreclem2  16433  prmreclem3  16434  1arith  16443  4sqlem11  16471  ramtlecl  16516  ramcl2lem  16525  ramxrcl  16533  prmgaplem3  16569  prmgaplem4  16570  cshwshashlem1  16612  structfn  16683  strleun  16775  srngbase  16812  srngplusg  16813  srngmulr  16814  lmodbase  16821  lmodplusg  16822  lmodsca  16823  ipsbase  16828  ipsaddg  16829  ipsmulr  16830  ipssca  16831  ipsvsca  16832  ipsip  16833  phlbase  16838  phlplusg  16839  phlsca  16840  phlvsca  16841  phlip  16842  odrngbas  16865  odrngplusg  16866  odrngmulr  16867  odrngtset  16868  odrngle  16869  odrngds  16870  prdsvallem  16913  prdsval  16914  prdssca  16915  prdsbas  16916  prdsplusg  16917  prdsmulr  16918  prdsvsca  16919  prdsip  16920  prdsle  16921  prdsds  16923  prdstset  16925  prdshom  16926  prdsco  16927  imasbas  16971  imasds  16972  imasplusg  16976  imasmulr  16977  imassca  16978  imasvsca  16979  imasip  16980  imastset  16981  imasle  16982  wunfunc  17359  wunfuncOLD  17360  fullfunc  17367  fthfunc  17368  isfull  17371  isfth  17375  wunnat  17417  wunnatOLD  17418  dmcoass  17526  catcisolem  17570  catciso  17571  catcoppccl  17577  catcoppcclOLD  17578  catcfuccl  17579  catcfucclOLD  17580  catcxpccl  17668  catcxpcclOLD  17669  ipobas  17991  ipolerval  17992  ipotset  17993  psdmrn  18033  psss  18040  ledm  18050  lern  18051  dirdm  18060  dirge  18063  mulgfval  18444  mvdco  18791  f1omvdconj  18792  gexex  19192  gsumval3  19246  lssacs  19958  cnfldbas  20321  cnfldadd  20322  cnfldmul  20323  cnfldcj  20324  cnfldtset  20325  cnfldle  20326  cnfldds  20327  cnfldunif  20328  rge0srg  20388  zntoslem  20475  asplss  20787  aspsubrg  20789  psrass1lemOLD  20853  psrass1lem  20856  psrbas  20857  psrplusg  20860  psrmulr  20863  psrsca  20868  psrvscafval  20869  psrass1  20884  psrass23l  20887  psrcom  20888  psrass23  20889  psropprmul  21113  coe1mul2  21144  ofco2  21302  toponsspwpw  21773  dmtopon  21774  leordtval2  22063  lmbrf  22111  lmres  22151  fiuncmp  22255  comppfsc  22383  1stckgenlem  22404  kgencn3  22409  ptbasfi  22432  xkoopn  22440  txcnmpt  22475  txkgen  22503  opnfbas  22693  fmfnfmlem4  22808  tsmsxplem1  23004  trust  23081  restutop  23089  nmoffn  23563  nmofval  23566  nmogelb  23568  nmolb  23569  nmof  23571  qtopbas  23611  tgqioo  23651  re2ndc  23652  iitopon  23730  dfii3  23734  iimulcn  23789  cnheiborlem  23805  bndth  23809  lebnumii  23817  reparphti  23848  pcoass  23875  cphsqrtcl  24035  lmmbrf  24113  iscauf  24131  caucfil  24134  lmclimf  24155  rrxmval  24256  rrxmet  24259  ovolfioo  24318  ovolficc  24319  ovolficcss  24320  ovolfsf  24322  ovollb  24330  ovolicc2lem3  24370  ovolicc2lem4  24371  ovolicc2  24373  volf  24380  volsup  24407  ovolfs2  24422  uniiccdif  24429  uniioovol  24430  uniiccvol  24431  uniioombllem2  24434  uniioombllem3a  24435  uniioombllem3  24436  uniioombllem4  24437  uniioombllem5  24438  uniioombl  24440  dyadmbllem  24450  dyadmbl  24451  opnmbllem  24452  opnmblALT  24454  volsup2  24456  vitalilem4  24462  vitalilem5  24463  vitali  24464  mbfimaopnlem  24506  mbflimsup  24517  i1f0  24538  i1f1  24541  itg11  24542  itg2mulc  24599  itg2gt0  24612  ellimc2  24728  limcresi  24736  dvreslem  24760  dvres2lem  24761  dvaddbr  24789  dvmulbr  24790  dvlipcn  24845  c1liplem1  24847  lhop1lem  24864  lhop1  24865  lhop2  24866  lhop  24867  dvfsumrlim  24882  ftc1cn  24894  itgsubstlem  24899  itgsubst  24900  itgpowd  24901  mdegleb  24916  mdeglt  24917  mdegldg  24918  mdegxrcl  24919  mdegcl  24921  mdegaddle  24926  mdegmullem  24930  deg1mul3le  24968  ig1peu  25023  ig1pdvds  25028  aacjcl  25174  aannenlem2  25176  aannenlem3  25177  aalioulem2  25180  taylfval  25205  radcnvcl  25263  radcnvlt1  25264  radcnvle  25266  abelth  25287  abelth2  25288  pilem2  25298  pilem3  25299  pige3ALT  25363  recosf1o  25378  resinf1o  25379  tanord1  25380  logcn  25489  dvlog  25493  dvlog2lem  25494  efopn  25500  logtayl  25502  cxpcn3  25588  loglesqrt  25598  ssscongptld  25659  leibpi  25779  efrlim  25806  jensenlem1  25823  jensenlem2  25824  jensen  25825  amgm  25827  lgamgulmlem2  25866  ftalem5  25913  efnnfsumcl  25939  efchtdvds  25995  dvdsmulf1o  26030  fsumdvdsmul  26031  lgsfcl2  26138  2sqlem6  26258  2sqlem8  26261  2sqlem9  26262  rpvmasumlem  26322  rpvmasum2  26347  dchrisum0re  26348  dchrisum0lem3  26354  dchrisum0  26355  rplogsum  26362  dirith2  26363  axtgcgrrflx  26507  axtgcgrid  26508  axtgsegcon  26509  axtg5seg  26510  axtgbtwnid  26511  axtgpasch  26512  axtgcont1  26513  tgcgr4  26576  motcgrg  26589  tglng  26591  upgrss  27133  pthdivtx  27770  disjxwwlkn  27951  ex-fpar  28499  nmlno0lem  28828  hlimcaui  29271  chsspwh  29282  shsss  29348  chintcli  29366  shsleji  29405  shub1i  29409  shsval2i  29422  lejdii  29573  spanuni  29579  sshhococi  29581  spansnpji  29613  osumcori  29678  5oai  29696  3oalem6  29702  3oai  29703  pjssmii  29716  mayete3i  29763  mayetes3i  29764  nmlnop0iALT  30030  imaelshi  30093  pjnmopi  30183  pjclem1  30230  pjci  30235  mdslmd1lem1  30360  shatomistici  30396  hatomistici  30397  chpssati  30398  xppreima  30656  iundisjfi  30791  iundisj2fi  30792  fprodex01  30813  xrsmulgzz  30960  fsumrp0cl  30977  gsummpt2co  30981  cycpmfv2  31054  cycpmrn  31083  xrge0slmod  31216  lsmsnorb  31247  idlsrgbas  31317  idlsrgplusg  31318  idlsrgmulr  31320  idlsrgtset  31321  ordtconnlem1  31542  xrge0iifhom  31555  lmlimxrge0  31566  lmxrge0  31570  indsumin  31656  esumcst  31697  esumpfinvallem  31708  esumpfinval  31709  esumpfinvalf  31710  esumcvg  31720  imambfm  31895  elmbfmvol2  31900  sxbrsigalem3  31905  sxbrsigalem2  31919  sxbrsigalem4  31920  sitgclg  31975  eulerpartlem1  32000  eulerpartlemgvv  32009  eulerpartlemgh  32011  eulerpartlemgf  32012  ballotlemfc0  32125  ballotlemfcc  32126  ballotlemiex  32134  ballotlemsup  32137  ballotlemsima  32148  ballotlemrv2  32154  ballotth  32170  signsplypnf  32195  signsply0  32196  rpsqrtcn  32239  itgexpif  32252  fsum2dsub  32253  reprfi2  32269  chtvalz  32275  breprexplemc  32278  breprexpnat  32280  circlemeth  32286  circlemethnat  32287  circlevma  32288  circlemethhgt  32289  hgt750lemd  32294  hgt750lema  32303  tgoldbachgtde  32306  tgoldbachgtda  32307  tgoldbachgt  32309  bnj1145  32640  bnj1286  32666  subfacp1lem2a  32809  erdszelem4  32823  erdszelem5  32824  erdszelem7  32826  erdszelem8  32827  kur14lem7  32841  kur14lem9  32843  cvxpconn  32871  cvxsconn  32872  resconn  32875  iccllysconn  32879  noextendseq  33556  oldf  33727  leftssno  33749  rightssno  33750  txpss3v  33866  txprel  33867  limitssson  33899  finminlem  34193  tailf  34250  filnetlem3  34255  onint1  34324  bj-unrab  34800  bj-2upln1upl  34900  bj-imdirco  35045  bj-rvecssabl  35160  taupilem2  35176  taupi  35177  poimirlem3  35466  poimirlem30  35493  poimirlem31  35494  poimirlem32  35495  broucube  35497  opnmbllem0  35499  mblfinlem1  35500  mblfinlem2  35501  mblfinlem3  35502  mblfinlem4  35503  ismblfin  35504  mbfposadd  35510  cnambfre  35511  itg2addnc  35517  ftc1cnnclem  35534  ftc1cnnc  35535  ftc1anclem3  35538  ftc1anclem7  35542  ftc1anc  35544  ftc2nc  35545  dvreasin  35549  dvreacos  35550  areacirclem1  35551  areacirclem2  35552  areacirc  35556  caures  35604  reheibor  35683  xrnss3v  36188  xrnrel  36189  atlatmstc  37019  atlatle  37020  pmaple  37461  sspadd1  37515  sspadd2  37516  dvrelog2  39754  dvrelog3  39755  diophin  40238  4rexfrabdioph  40264  6rexfrabdioph  40265  irrapxlem1  40288  irrapx1  40294  monotuz  40407  jm2.27dlem5  40479  hbtlem2  40593  algbase  40647  algaddg  40648  algmulr  40649  algsca  40650  algvsca  40651  arearect  40690  areaquad  40691  rtrclex  40842  trclubgNEW  40843  trclexi  40845  rtrclexi  40846  cnvtrcl0  40851  dfrtrcl5  40854  trrelsuperrel2dg  40897  relexpaddss  40944  brtrclfv2  40953  frege131d  40990  xphe  41007  clsk3nimkb  41268  gneispace  41362  k0004val0  41382  inaex  41529  lhe4.4ex1a  41561  uzmptshftfval  41578  binomcxplemdvbinom  41585  binomcxplemcvg  41586  binomcxplemnotnn0  41588  relopabVD  42135  fzisoeu  42453  fzsscn  42464  fzssre  42467  fzossuz  42534  zssxr  42551  uzssre2  42561  supminfxr  42620  uzsscn  42632  rpssxr  42637  uzinico  42714  limcresiooub  42801  limcresioolb  42802  limcleqr  42803  limclner  42810  limclr  42814  limsupequzmpt2  42877  liminfval2  42927  liminfequzmpt2  42950  icccncfext  43046  cncficcgt0  43047  ioodvbdlimc1lem2  43091  ioodvbdlimc2lem  43093  dvnprodlem1  43105  dvnprodlem2  43106  itgsin0pilem1  43109  itgsinexplem1  43113  itgsinexp  43114  dirkercncflem2  43263  fourierdlem16  43282  fourierdlem18  43284  fourierdlem20  43286  fourierdlem21  43287  fourierdlem22  43288  fourierdlem25  43291  fourierdlem37  43303  fourierdlem42  43308  fourierdlem50  43315  fourierdlem52  43317  fourierdlem62  43327  fourierdlem64  43329  fourierdlem66  43331  fourierdlem68  43333  fourierdlem74  43339  fourierdlem75  43340  fourierdlem76  43341  fourierdlem79  43344  fourierdlem83  43348  fourierdlem95  43360  fourierdlem101  43366  fourierdlem102  43367  fourierdlem103  43368  fourierdlem104  43369  fourierdlem112  43377  fourierdlem114  43379  sqwvfoura  43387  sqwvfourb  43388  fouriersw  43390  etransclem24  43417  etransclem48  43441  sge0sn  43535  sge0tsms  43536  sge0f1o  43538  sge0pr  43550  sge0resplit  43562  sge0split  43565  sge0iunmptlemre  43571  sge0isummpt2  43588  carageniuncllem1  43677  hoicvr  43704  hoicvrrex  43712  hoidmvlelem2  43752  hspmbl  43785  smfmullem4  43943  prmdvdsfmtnof1lem1  44652  prmdvdsfmtnof  44654  oddibas  44983  2zrngbas  45110  2zrng0  45112  sepfsepc  45837  aacllem  46119  amgmlemALT  46121