Theorem sstri 3206

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

Syntax hints:   ⊆ wss 3170

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 1471  ax-7 1472  ax-gen 1473  ax-ie1 1517  ax-ie2 1518  ax-8 1528  ax-11 1530  ax-4 1534  ax-17 1550  ax-i9 1554  ax-ial 1558  ax-i5r 1559  ax-ext 2188

This theorem depends on definitions:  df-bi 117  df-nf 1485  df-sb 1787  df-clab 2193  df-cleq 2199  df-clel 2202  df-in 3176  df-ss 3183

This theorem is referenced by:  difdif2ss  3434  difdifdirss  3549  snsstp1  3789  snsstp2  3790  nnregexmid  4677  dmexg  4951  rnexg  4952  ssrnres  5134  cossxp  5214  cocnvss  5217  funinsn  5332  fabexg  5475  foimacnv  5552  ssimaex  5653  oprabss  6044  tposssxp  6348  mapsspw  6784  sbthlemi5  7078  sbthlem7  7080  caserel  7204  dmaddpi  7458  dmmulpi  7459  ltrelxr  8153  nnsscn  9061  nn0sscn  9320  nn0ssq  9769  nnssq  9770  qsscn  9772  fzval2  10153  fzossnn  10335  fzo0ssnn0  10366  infssuzcldc  10400  expcl2lemap  10718  rpexpcl  10725  expge0  10742  expge1  10743  seq3coll  11009  summodclem2a  11767  fsum3cvg3  11782  fsumrpcl  11790  fsumge0  11845  prodmodclem2a  11962  fprodrpcl  11997  fprodge0  12023  fprodge1  12025  nninfctlemfo  12436  isprm3  12515  eulerthlemrprm  12626  eulerthlema  12627  eulerthlemh  12628  eulerthlemth  12629  pcprecl  12687  pcprendvds  12688  pcpremul  12691  4sqlem11  12799  structfn  12926  strleun  13011  prdsvallem  13179  prdsval  13180  prdssca  13182  prdsbas  13183  prdsplusg  13184  prdsmulr  13185  cnfldbas  14397  mpocnfldadd  14398  mpocnfldmul  14400  cnfldcj  14402  cnfldtset  14403  cnfldle  14404  cnfldds  14405  psrplusgg  14515  toponsspwpwg  14569  dmtopon  14570  lmbrf  14762  lmres  14795  txcnmpt  14820  qtopbas  15069  tgqioo  15102  dvrecap  15260  cosz12  15327  ioocosf1o  15401  mpodvdsmulf1o  15537  fsumdvdsmul  15538  lgsfcl2  15558  2sqlem6  15672  2sqlem8  15675  2sqlem9  15676