Theorem sstri 3193

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 3191	. 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  3421  difdifdirss  3536  snsstp1  3773  snsstp2  3774  nnregexmid  4658  dmexg  4931  rnexg  4932  ssrnres  5113  cossxp  5193  cocnvss  5196  funinsn  5308  fabexg  5448  foimacnv  5525  ssimaex  5625  oprabss  6012  tposssxp  6316  mapsspw  6752  sbthlemi5  7036  sbthlem7  7038  caserel  7162  dmaddpi  7409  dmmulpi  7410  ltrelxr  8104  nnsscn  9012  nn0sscn  9271  nn0ssq  9719  nnssq  9720  qsscn  9722  fzval2  10103  fzossnn  10282  fzo0ssnn0  10308  infssuzcldc  10342  expcl2lemap  10660  rpexpcl  10667  expge0  10684  expge1  10685  seq3coll  10951  summodclem2a  11563  fsum3cvg3  11578  fsumrpcl  11586  fsumge0  11641  prodmodclem2a  11758  fprodrpcl  11793  fprodge0  11819  fprodge1  11821  nninfctlemfo  12232  isprm3  12311  eulerthlemrprm  12422  eulerthlema  12423  eulerthlemh  12424  eulerthlemth  12425  pcprecl  12483  pcprendvds  12484  pcpremul  12487  4sqlem11  12595  structfn  12722  strleun  12807  prdsvallem  12974  prdsval  12975  prdssca  12977  prdsbas  12978  prdsplusg  12979  prdsmulr  12980  cnfldbas  14192  mpocnfldadd  14193  mpocnfldmul  14195  cnfldcj  14197  cnfldtset  14198  cnfldle  14199  cnfldds  14200  psrplusgg  14306  toponsspwpwg  14342  dmtopon  14343  lmbrf  14535  lmres  14568  txcnmpt  14593  qtopbas  14842  tgqioo  14875  dvrecap  15033  cosz12  15100  ioocosf1o  15174  mpodvdsmulf1o  15310  fsumdvdsmul  15311  lgsfcl2  15331  2sqlem6  15445  2sqlem8  15448  2sqlem9  15449