Theorem sstri 3192

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

Syntax hints:   ⊆ wss 3157

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 1461  ax-7 1462  ax-gen 1463  ax-ie1 1507  ax-ie2 1508  ax-8 1518  ax-11 1520  ax-4 1524  ax-17 1540  ax-i9 1544  ax-ial 1548  ax-i5r 1549  ax-ext 2178

This theorem depends on definitions:  df-bi 117  df-nf 1475  df-sb 1777  df-clab 2183  df-cleq 2189  df-clel 2192  df-in 3163  df-ss 3170

This theorem is referenced by:  difdif2ss  3420  difdifdirss  3535  snsstp1  3772  snsstp2  3773  nnregexmid  4657  dmexg  4930  rnexg  4931  ssrnres  5112  cossxp  5192  cocnvss  5195  funinsn  5307  fabexg  5445  foimacnv  5522  ssimaex  5622  oprabss  6008  tposssxp  6307  mapsspw  6743  sbthlemi5  7027  sbthlem7  7029  caserel  7153  dmaddpi  7392  dmmulpi  7393  ltrelxr  8087  nnsscn  8995  nn0sscn  9254  nn0ssq  9702  nnssq  9703  qsscn  9705  fzval2  10086  fzossnn  10265  fzo0ssnn0  10291  infssuzcldc  10325  expcl2lemap  10643  rpexpcl  10650  expge0  10667  expge1  10668  seq3coll  10934  summodclem2a  11546  fsum3cvg3  11561  fsumrpcl  11569  fsumge0  11624  prodmodclem2a  11741  fprodrpcl  11776  fprodge0  11802  fprodge1  11804  nninfctlemfo  12207  isprm3  12286  eulerthlemrprm  12397  eulerthlema  12398  eulerthlemh  12399  eulerthlemth  12400  pcprecl  12458  pcprendvds  12459  pcpremul  12462  4sqlem11  12570  structfn  12697  strleun  12782  cnfldbas  14116  mpocnfldadd  14117  mpocnfldmul  14119  cnfldcj  14121  cnfldtset  14122  cnfldle  14123  cnfldds  14124  psrplusgg  14230  toponsspwpwg  14258  dmtopon  14259  lmbrf  14451  lmres  14484  txcnmpt  14509  qtopbas  14758  tgqioo  14791  dvrecap  14949  cosz12  15016  ioocosf1o  15090  mpodvdsmulf1o  15226  fsumdvdsmul  15227  lgsfcl2  15247  2sqlem6  15361  2sqlem8  15364  2sqlem9  15365