Theorem sstri 3035

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

Syntax hints:   ⊆ wss 3000

This theorem was proved from axioms:  ax-1 5  ax-2 6  ax-mp 7  ax-ia1 105  ax-ia2 106  ax-ia3 107  ax-5 1382  ax-7 1383  ax-gen 1384  ax-ie1 1428  ax-ie2 1429  ax-8 1441  ax-11 1443  ax-4 1446  ax-17 1465  ax-i9 1469  ax-ial 1473  ax-i5r 1474  ax-ext 2071

This theorem depends on definitions:  df-bi 116  df-nf 1396  df-sb 1694  df-clab 2076  df-cleq 2082  df-clel 2085  df-in 3006  df-ss 3013

This theorem is referenced by:  difdif2ss  3257  difdifdirss  3371  snsstp1  3593  snsstp2  3594  nnregexmid  4447  dmexg  4710  rnexg  4711  ssrnres  4886  cossxp  4966  cocnvss  4969  funinsn  5076  fabexg  5211  foimacnv  5284  ssimaex  5378  oprabss  5748  tposssxp  6028  mapsspw  6455  sbthlemi5  6724  sbthlem7  6726  djuin  6810  caserel  6832  dmaddpi  6945  dmmulpi  6946  ltrelxr  7608  nnsscn  8488  nn0sscn  8739  nn0ssq  9174  nnssq  9175  qsscn  9177  fzval2  9488  fzossnn  9661  fzo0ssnn0  9687  expcl2lemap  10028  rpexpcl  10035  expge0  10052  expge1  10053  iseqcoll  10308  isummolem2a  10832  fsum3cvg3  10850  fsumrpcl  10859  fsumge0  10914  infssuzcldc  11286  isprm3  11439  structfn  11574  strleun  11644  toponsspwpwg  11781  dmtopon  11782