Theorem sstri 3156

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

Syntax hints:   ⊆ wss 3121

This theorem was proved from axioms:  ax-mp 5  ax-1 6  ax-2 7  ax-ia1 105  ax-ia2 106  ax-ia3 107  ax-5 1440  ax-7 1441  ax-gen 1442  ax-ie1 1486  ax-ie2 1487  ax-8 1497  ax-11 1499  ax-4 1503  ax-17 1519  ax-i9 1523  ax-ial 1527  ax-i5r 1528  ax-ext 2152

This theorem depends on definitions:  df-bi 116  df-nf 1454  df-sb 1756  df-clab 2157  df-cleq 2163  df-clel 2166  df-in 3127  df-ss 3134

This theorem is referenced by:  difdif2ss  3384  difdifdirss  3498  snsstp1  3728  snsstp2  3729  nnregexmid  4603  dmexg  4873  rnexg  4874  ssrnres  5051  cossxp  5131  cocnvss  5134  funinsn  5245  fabexg  5383  foimacnv  5458  ssimaex  5555  oprabss  5936  tposssxp  6225  mapsspw  6658  sbthlemi5  6934  sbthlem7  6936  caserel  7060  dmaddpi  7274  dmmulpi  7275  ltrelxr  7967  nnsscn  8870  nn0sscn  9127  nn0ssq  9574  nnssq  9575  qsscn  9577  fzval2  9955  fzossnn  10132  fzo0ssnn0  10158  expcl2lemap  10475  rpexpcl  10482  expge0  10499  expge1  10500  seq3coll  10764  summodclem2a  11331  fsum3cvg3  11346  fsumrpcl  11354  fsumge0  11409  prodmodclem2a  11526  fprodrpcl  11561  fprodge0  11587  fprodge1  11589  infssuzcldc  11893  isprm3  12059  eulerthlemrprm  12170  eulerthlema  12171  eulerthlemh  12172  eulerthlemth  12173  pcprecl  12230  pcprendvds  12231  pcpremul  12234  structfn  12422  strleun  12494  toponsspwpwg  12773  dmtopon  12774  lmbrf  12968  lmres  13001  txcnmpt  13026  qtopbas  13275  tgqioo  13300  dvrecap  13430  cosz12  13454  ioocosf1o  13528  lgsfcl2  13660  2sqlem6  13709  2sqlem8  13712  2sqlem9  13713