Theorem sstri 3178

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

Syntax hints:   ⊆ wss 3143

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 1457  ax-7 1458  ax-gen 1459  ax-ie1 1503  ax-ie2 1504  ax-8 1514  ax-11 1516  ax-4 1520  ax-17 1536  ax-i9 1540  ax-ial 1544  ax-i5r 1545  ax-ext 2170

This theorem depends on definitions:  df-bi 117  df-nf 1471  df-sb 1773  df-clab 2175  df-cleq 2181  df-clel 2184  df-in 3149  df-ss 3156

This theorem is referenced by:  difdif2ss  3406  difdifdirss  3521  snsstp1  3756  snsstp2  3757  nnregexmid  4634  dmexg  4905  rnexg  4906  ssrnres  5085  cossxp  5165  cocnvss  5168  funinsn  5279  fabexg  5417  foimacnv  5493  ssimaex  5592  oprabss  5976  tposssxp  6267  mapsspw  6701  sbthlemi5  6977  sbthlem7  6979  caserel  7103  dmaddpi  7341  dmmulpi  7342  ltrelxr  8035  nnsscn  8941  nn0sscn  9198  nn0ssq  9645  nnssq  9646  qsscn  9648  fzval2  10028  fzossnn  10206  fzo0ssnn0  10232  expcl2lemap  10549  rpexpcl  10556  expge0  10573  expge1  10574  seq3coll  10839  summodclem2a  11406  fsum3cvg3  11421  fsumrpcl  11429  fsumge0  11484  prodmodclem2a  11601  fprodrpcl  11636  fprodge0  11662  fprodge1  11664  infssuzcldc  11969  isprm3  12135  eulerthlemrprm  12246  eulerthlema  12247  eulerthlemh  12248  eulerthlemth  12249  pcprecl  12306  pcprendvds  12307  pcpremul  12310  structfn  12498  strleun  12581  cnfldbas  13828  cnfldadd  13829  cnfldmul  13830  toponsspwpwg  13905  dmtopon  13906  lmbrf  14098  lmres  14131  txcnmpt  14156  qtopbas  14405  tgqioo  14430  dvrecap  14560  cosz12  14584  ioocosf1o  14658  lgsfcl2  14790  2sqlem6  14850  2sqlem8  14853  2sqlem9  14854