Theorem sstri 3165

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

Syntax hints:   ⊆ wss 3130

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 1447  ax-7 1448  ax-gen 1449  ax-ie1 1493  ax-ie2 1494  ax-8 1504  ax-11 1506  ax-4 1510  ax-17 1526  ax-i9 1530  ax-ial 1534  ax-i5r 1535  ax-ext 2159

This theorem depends on definitions:  df-bi 117  df-nf 1461  df-sb 1763  df-clab 2164  df-cleq 2170  df-clel 2173  df-in 3136  df-ss 3143

This theorem is referenced by:  difdif2ss  3393  difdifdirss  3508  snsstp1  3743  snsstp2  3744  nnregexmid  4621  dmexg  4892  rnexg  4893  ssrnres  5072  cossxp  5152  cocnvss  5155  funinsn  5266  fabexg  5404  foimacnv  5480  ssimaex  5578  oprabss  5961  tposssxp  6250  mapsspw  6684  sbthlemi5  6960  sbthlem7  6962  caserel  7086  dmaddpi  7324  dmmulpi  7325  ltrelxr  8018  nnsscn  8924  nn0sscn  9181  nn0ssq  9628  nnssq  9629  qsscn  9631  fzval2  10011  fzossnn  10189  fzo0ssnn0  10215  expcl2lemap  10532  rpexpcl  10539  expge0  10556  expge1  10557  seq3coll  10822  summodclem2a  11389  fsum3cvg3  11404  fsumrpcl  11412  fsumge0  11467  prodmodclem2a  11584  fprodrpcl  11619  fprodge0  11645  fprodge1  11647  infssuzcldc  11952  isprm3  12118  eulerthlemrprm  12229  eulerthlema  12230  eulerthlemh  12231  eulerthlemth  12232  pcprecl  12289  pcprendvds  12290  pcpremul  12293  structfn  12481  strleun  12563  cnfldbas  13462  cnfldadd  13463  cnfldmul  13464  toponsspwpwg  13525  dmtopon  13526  lmbrf  13718  lmres  13751  txcnmpt  13776  qtopbas  14025  tgqioo  14050  dvrecap  14180  cosz12  14204  ioocosf1o  14278  lgsfcl2  14410  2sqlem6  14470  2sqlem8  14473  2sqlem9  14474