Theorem sstri 3251

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

Syntax hints:   ⊆ wss 3214

This theorem was proved from axioms:  ax-mp 5  ax-1 6  ax-2 7  ax-ia1 106  ax-ia2 107  ax-ia3 108  ax-5 1496  ax-7 1497  ax-gen 1498  ax-ie1 1542  ax-ie2 1543  ax-8 1553  ax-11 1555  ax-4 1559  ax-17 1575  ax-i9 1579  ax-ial 1583  ax-i5r 1584  ax-ext 2216

This theorem depends on definitions:  df-bi 117  df-nf 1510  df-sb 1812  df-clab 2221  df-cleq 2227  df-clel 2230  df-in 3220  df-ss 3227

This theorem is referenced by:  difdif2ss  3482  difdifdirss  3598  snsstp1  3849  snsstp2  3850  elopabran  4407  nnregexmid  4748  dmexg  5026  rnexg  5027  ssrnres  5210  cossxp  5290  cocnvss  5293  funinsn  5410  fabexg  5559  foimacnv  5637  ssimaex  5743  oprabss  6147  tposssxp  6493  mapsspw  6931  sbthlemi5  7244  sbthlem7  7246  caserel  7391  dmaddpi  7656  dmmulpi  7657  ltrelxr  8350  nnsscn  9259  nn0sscn  9518  nn0ssq  9978  nnssq  9979  qsscn  9981  fzval2  10364  fzossnn  10551  fzo0ssnn0  10582  infssuzcldc  10617  expcl2lemap  10937  rpexpcl  10944  expge0  10961  expge1  10962  seq3coll  11239  summodclem2a  12092  fsum3cvg3  12107  fsumrpcl  12115  fsumge0  12170  prodmodclem2a  12287  fprodrpcl  12322  fprodge0  12348  fprodge1  12350  nninfctlemfo  12761  isprm3  12840  eulerthlemrprm  12951  eulerthlema  12952  eulerthlemh  12953  eulerthlemth  12954  pcprecl  13012  pcprendvds  13013  pcpremul  13016  4sqlem11  13124  ballotfilemfc0  13176  ballotfilemfcc  13177  ballotfilemiex  13188  ballotfilemsima  13203  structfn  13315  strleun  13401  prdsvallem  13564  prdsval  14115  prdssca  14117  prdsbas  14118  prdsplusg  14119  prdsmulr  14120  cnfldbas  14834  mpocnfldadd  14835  mpocnfldmul  14837  cnfldcj  14839  cnfldtset  14840  cnfldle  14841  cnfldds  14842  psrplusgg  14959  toponsspwpwg  15013  dmtopon  15014  lmbrf  15206  lmres  15239  txcnmpt  15264  qtopbas  15513  tgqioo  15546  dvrecap  15704  cosz12  15771  ioocosf1o  15845  mpodvdsmulf1o  15984  fsumdvdsmul  15985  lgsfcl2  16005  2sqlem6  16119  2sqlem8  16122  2sqlem9  16123  trlsex  16508  eupthsg  16566