Theorem sstri 3893

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

Syntax hints:   ⊆ wss 3854

This theorem was proved from axioms:  ax-mp 5  ax-1 6  ax-2 7  ax-3 8  ax-gen 1775  ax-4 1789  ax-5 1886  ax-6 1945  ax-7 1990  ax-8 2081  ax-9 2089  ax-10 2110  ax-11 2124  ax-12 2139  ax-ext 2767

This theorem depends on definitions:  df-bi 208  df-an 397  df-or 843  df-tru 1523  df-ex 1760  df-nf 1764  df-sb 2041  df-clab 2774  df-cleq 2786  df-clel 2861  df-in 3861  df-ss 3869

This theorem is referenced by:  snsstp1  4650  snsstp2  4651  uniintsn  4813  ssrnres  5903  cossxp  5990  foimacnv  6492  ssimaex  6607  riotassuni  7005  oprabss  7107  dmexg  7460  rnexg  7461  fabexg  7486  fparlem3  7656  fparlem4  7657  snopsuppss  7687  tposssxp  7738  mapsspw  8283  sbthlem5  8468  sbthlem7  8470  cnvimamptfin  8661  marypha1lem  8733  ordtypelem4  8821  hartogslem1  8842  tc2  9019  tz9.12lem1  9051  rankval4  9131  rankxpl  9139  rankmapu  9142  rankxplim  9143  djuin  9182  infxpenlem  9274  ackbij1lem18  9494  cflm  9507  fin23lem29  9598  hsmexlem4  9686  hsmexlem5  9687  brdom3  9785  brdom5  9786  brdom4  9787  smobeth  9843  pwfseqlem3  9917  wundm  9985  wunrn  9986  wunex2  9995  ltsopi  10145  dmaddpi  10147  dmmulpi  10148  nqerf  10187  ltrelxr  10538  uzwo2  12150  infssuzle  12169  infssuzcl  12170  uzwo3  12181  nn0ssq  12195  nnssq  12196  qsscn  12198  rpnnen1lem3  12217  rpnnen1lem5  12219  dflt2  12380  fzval2  12734  fzossnn  12924  injresinj  12996  flval3  13023  uzsup  13069  uzrdgfni  13164  expcl2lem  13279  rpexpcl  13286  expge0  13303  expge1  13304  hashxrcl  13556  seqcoll  13658  wrdexgOLD  13706  xptrrel  14162  trclublem  14177  sqrlem3  14426  limsupval2  14659  limsupgre  14660  rlimpm  14679  rlimclim  14725  isercolllem1  14843  isercolllem2  14844  isercoll  14846  caurcvg  14855  caucvg  14857  summolem2a  14893  summolem2  14894  zsum  14896  fsumcvg3  14907  fsumrpcl  14915  fsumge0  14971  climfsum  14996  ackbijnn  15004  prodmolem2a  15109  prodmolem2  15110  zprod  15112  fprodrpcl  15131  fprodge0  15168  fprodge1  15170  rprisefaccl  15198  divalglem8  15572  sadaddlem  15636  lcmfval  15782  isprm3  15844  maxprmfct  15870  pclem  15992  prmreclem1  16069  prmreclem2  16070  prmreclem3  16071  1arith  16080  4sqlem11  16108  ramtlecl  16153  ramcl2lem  16162  ramxrcl  16170  prmgaplem3  16206  prmgaplem4  16207  cshwshashlem1  16246  structfn  16317  strleun  16408  srngbase  16445  srngplusg  16446  srngmulr  16447  lmodbase  16454  lmodplusg  16455  lmodsca  16456  ipsbase  16461  ipsaddg  16462  ipsmulr  16463  ipssca  16464  ipsvsca  16465  ipsip  16466  phlbase  16471  phlplusg  16472  phlsca  16473  phlvsca  16474  phlip  16475  odrngbas  16497  odrngplusg  16498  odrngmulr  16499  odrngtset  16500  odrngle  16501  odrngds  16502  prdsval  16545  prdssca  16546  prdsbas  16547  prdsplusg  16548  prdsmulr  16549  prdsvsca  16550  prdsip  16551  prdsle  16552  prdsds  16554  prdstset  16556  prdshom  16557  prdsco  16558  imasbas  16602  imasds  16603  imasplusg  16607  imasmulr  16608  imassca  16609  imasvsca  16610  imasip  16611  imastset  16612  imasle  16613  wunfunc  16986  fullfunc  16993  fthfunc  16994  isfull  16997  isfth  17001  wunnat  17043  dmcoass  17143  catcisolem  17183  catciso  17184  catcoppccl  17185  catcfuccl  17186  catcxpccl  17274  ipobas  17582  ipolerval  17583  ipotset  17584  psdmrn  17634  psss  17641  ledm  17651  lern  17652  dirdm  17661  dirge  17664  mulgfval  17971  mvdco  18292  f1omvdconj  18293  gexex  18684  gsumval3  18736  lssacs  19417  asplss  19779  aspsubrg  19781  psrass1lem  19833  psrbas  19834  psrplusg  19837  psrmulr  19840  psrsca  19845  psrvscafval  19846  psrass1  19861  psrass23l  19864  psrcom  19865  psrass23  19866  psropprmul  20077  coe1mul2  20108  cnfldbas  20219  cnfldadd  20220  cnfldmul  20221  cnfldcj  20222  cnfldtset  20223  cnfldle  20224  cnfldds  20225  cnfldunif  20226  rge0srg  20286  zntoslem  20373  ofco2  20732  toponsspwpw  21202  dmtopon  21203  leordtval2  21492  lmbrf  21540  lmres  21580  fiuncmp  21684  comppfsc  21812  1stckgenlem  21833  kgencn3  21838  ptbasfi  21861  xkoopn  21869  txcnmpt  21904  txkgen  21932  opnfbas  22122  fmfnfmlem4  22237  tsmsxplem1  22432  trust  22509  restutop  22517  nmoffn  22991  nmofval  22994  nmogelb  22996  nmolb  22997  nmof  22999  qtopbas  23039  tgqioo  23079  re2ndc  23080  iitopon  23158  dfii3  23162  iimulcn  23213  cnheiborlem  23229  bndth  23233  lebnumii  23241  reparphti  23272  pcoass  23299  cphsqrtcl  23459  lmmbrf  23536  iscauf  23554  caucfil  23557  lmclimf  23578  rrxmval  23679  rrxmet  23682  ovolfioo  23739  ovolficc  23740  ovolficcss  23741  ovolfsf  23743  ovollb  23751  ovolicc2lem3  23791  ovolicc2lem4  23792  ovolicc2  23794  volf  23801  volsup  23828  ovolfs2  23843  uniiccdif  23850  uniioovol  23851  uniiccvol  23852  uniioombllem2  23855  uniioombllem3a  23856  uniioombllem3  23857  uniioombllem4  23858  uniioombllem5  23859  uniioombl  23861  dyadmbllem  23871  dyadmbl  23872  opnmbllem  23873  opnmblALT  23875  volsup2  23877  vitalilem4  23883  vitalilem5  23884  vitali  23885  mbfimaopnlem  23927  mbflimsup  23938  i1f0  23959  i1f1  23962  itg11  23963  itg2mulc  24019  itg2gt0  24032  ellimc2  24146  limcresi  24154  dvreslem  24178  dvres2lem  24179  dvaddbr  24206  dvmulbr  24207  dvlipcn  24262  c1liplem1  24264  lhop1lem  24281  lhop1  24282  lhop2  24283  lhop  24284  dvfsumrlim  24299  ftc1cn  24311  itgsubstlem  24316  itgsubst  24317  mdegleb  24329  mdeglt  24330  mdegldg  24331  mdegxrcl  24332  mdegcl  24334  mdegaddle  24339  mdegmullem  24343  deg1mul3le  24381  ig1peu  24436  ig1pdvds  24441  aacjcl  24587  aannenlem2  24589  aannenlem3  24590  aalioulem2  24593  taylfval  24618  radcnvcl  24676  radcnvlt1  24677  radcnvle  24679  abelth  24700  abelth2  24701  pilem2  24711  pilem3  24712  pige3ALT  24776  recosf1o  24788  resinf1o  24789  tanord1  24790  logcn  24899  dvlog  24903  dvlog2lem  24904  efopn  24910  logtayl  24912  cxpcn3  24998  loglesqrt  25008  ssscongptld  25069  leibpi  25190  efrlim  25217  jensenlem1  25234  jensenlem2  25235  jensen  25236  amgm  25238  lgamgulmlem2  25277  ftalem5  25324  efnnfsumcl  25350  efchtdvds  25406  dvdsmulf1o  25441  fsumdvdsmul  25442  lgsfcl2  25549  2sqlem6  25669  2sqlem8  25672  2sqlem9  25673  rpvmasumlem  25733  rpvmasum2  25758  dchrisum0re  25759  dchrisum0lem3  25765  dchrisum0  25766  rplogsum  25773  dirith2  25774  axtgcgrrflx  25918  axtgcgrid  25919  axtgsegcon  25920  axtg5seg  25921  axtgbtwnid  25922  axtgpasch  25923  axtgcont1  25924  tgcgr4  25987  motcgrg  26000  tglng  26002  upgrss  26544  pthdivtx  27185  disjxwwlkn  27367  nmlno0lem  28249  hlimcaui  28692  chsspwh  28703  shsss  28769  chintcli  28787  shsleji  28826  shub1i  28830  shsval2i  28843  lejdii  28994  spanuni  29000  sshhococi  29002  spansnpji  29034  osumcori  29099  5oai  29117  3oalem6  29123  3oai  29124  pjssmii  29137  mayete3i  29184  mayetes3i  29185  nmlnop0iALT  29451  imaelshi  29514  pjnmopi  29604  pjclem1  29651  pjci  29656  mdslmd1lem1  29781  shatomistici  29817  hatomistici  29818  chpssati  29819  xppreima  30057  iundisjfi  30177  iundisj2fi  30178  fprodex01  30196  xrsmulgzz  30309  fsumrp0cl  30326  cycpmfv2  30367  gsummpt2co  30453  xrge0slmod  30526  unitsscn  30712  ordtconnlem1  30740  xrge0iifhom  30753  lmlimxrge0  30764  lmxrge0  30768  indsumin  30854  esumcst  30895  esumpfinvallem  30906  esumpfinval  30907  esumpfinvalf  30908  esumcvg  30918  imambfm  31093  elmbfmvol2  31098  sxbrsigalem3  31103  sxbrsigalem2  31117  sxbrsigalem4  31118  sitgclg  31173  eulerpartlem1  31198  eulerpartlemgvv  31207  eulerpartlemgh  31209  eulerpartlemgf  31210  ballotlemfc0  31323  ballotlemfcc  31324  ballotlemiex  31332  ballotlemsup  31335  ballotlemsdom  31342  ballotlemsima  31346  ballotlemrv2  31352  ballotth  31368  signsplypnf  31393  signsply0  31394  rpsqrtcn  31437  itgexpif  31450  fsum2dsub  31451  reprfi2  31467  chtvalz  31473  breprexplemc  31476  breprexpnat  31478  circlemeth  31484  circlemethnat  31485  circlevma  31486  circlemethhgt  31487  hgt750lemd  31492  hgt750lema  31501  tgoldbachgtde  31504  tgoldbachgtda  31505  tgoldbachgt  31507  bnj1145  31835  bnj1286  31861  subfacp1lem2a  31991  erdszelem4  32005  erdszelem5  32006  erdszelem7  32008  erdszelem8  32009  kur14lem7  32023  kur14lem9  32025  cvxpconn  32053  cvxsconn  32054  resconn  32057  iccllysconn  32061  noextendseq  32728  txpss3v  32893  txprel  32894  limitssson  32926  finminlem  33220  tailf  33277  filnetlem3  33282  onint1  33350  bj-unrab  33761  bj-2upln1upl  33887  bj-rrvecsscmn  34070  taupilem2  34080  taupi  34081  poimirlem3  34372  poimirlem30  34399  poimirlem31  34400  poimirlem32  34401  broucube  34403  opnmbllem0  34405  mblfinlem1  34406  mblfinlem2  34407  mblfinlem3  34408  mblfinlem4  34409  ismblfin  34410  mbfposadd  34416  cnambfre  34417  itg2addnc  34423  ftc1cnnclem  34442  ftc1cnnc  34443  ftc1anclem3  34446  ftc1anclem7  34450  ftc1anc  34452  ftc2nc  34453  dvreasin  34457  dvreacos  34458  areacirclem1  34459  areacirclem2  34460  areacirc  34464  caures  34513  reheibor  34595  xrnss3v  35105  xrnrel  35106  atlatmstc  35936  atlatle  35937  pmaple  36378  sspadd1  36432  sspadd2  36433  diophin  38805  4rexfrabdioph  38831  6rexfrabdioph  38832  irrapxlem1  38855  irrapx1  38861  monotuz  38974  jm2.27dlem5  39046  hbtlem2  39160  algbase  39214  algaddg  39215  algmulr  39216  algsca  39217  algvsca  39218  itgpowd  39257  arearect  39258  areaquad  39259  rtrclex  39413  trclubgNEW  39414  trclexi  39416  rtrclexi  39417  cnvtrcl0  39422  dfrtrcl5  39425  trrelsuperrel2dg  39452  relexpaddss  39499  brtrclfv2  39508  frege131d  39545  xphe  39563  clsk3nimkb  39826  gneispace  39920  k0004val0  39940  inaex  40082  lhe4.4ex1a  40151  uzmptshftfval  40168  binomcxplemdvbinom  40175  binomcxplemcvg  40176  binomcxplemnotnn0  40178  relopabVD  40726  fzisoeu  41061  fzsscn  41072  fzssre  41075  fzossuz  41144  fzossz  41145  uzssre  41164  zssxr  41165  uzssre2  41176  supminfxr  41236  uzsscn  41248  rpssxr  41253  ioosscn  41265  uzinico  41332  limcresiooub  41419  limcresioolb  41420  limcleqr  41421  limclner  41428  limclr  41432  limsupequzmpt2  41495  liminfval2  41545  liminfequzmpt2  41568  icccncfext  41665  cncficcgt0  41666  ioodvbdlimc1lem2  41712  ioodvbdlimc2lem  41714  dvnprodlem1  41726  dvnprodlem2  41727  itgsin0pilem1  41730  itgsinexplem1  41734  itgsinexp  41735  dirkercncflem2  41885  fourierdlem16  41904  fourierdlem18  41906  fourierdlem20  41908  fourierdlem21  41909  fourierdlem22  41910  fourierdlem25  41913  fourierdlem37  41925  fourierdlem42  41930  fourierdlem50  41937  fourierdlem52  41939  fourierdlem62  41949  fourierdlem64  41951  fourierdlem66  41953  fourierdlem68  41955  fourierdlem74  41961  fourierdlem75  41962  fourierdlem76  41963  fourierdlem79  41966  fourierdlem83  41970  fourierdlem95  41982  fourierdlem101  41988  fourierdlem102  41989  fourierdlem103  41990  fourierdlem104  41991  fourierdlem112  41999  fourierdlem114  42001  sqwvfoura  42009  sqwvfourb  42010  fouriersw  42012  etransclem24  42039  etransclem48  42063  sge0sn  42157  sge0tsms  42158  sge0f1o  42160  sge0pr  42172  sge0resplit  42184  sge0split  42187  sge0iunmptlemre  42193  sge0isummpt2  42210  carageniuncllem1  42299  hoicvr  42326  hoicvrrex  42334  hoidmvlelem2  42374  hspmbl  42407  smfmullem4  42565  prmdvdsfmtnof1lem1  43182  prmdvdsfmtnof  43184  oddibas  43516  2zrngbas  43639  2zrng0  43641  aacllem  44336  amgmlemALT  44338