Theorem sstri 3189

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

Syntax hints:   ⊆ wss 3154

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 1458  ax-7 1459  ax-gen 1460  ax-ie1 1504  ax-ie2 1505  ax-8 1515  ax-11 1517  ax-4 1521  ax-17 1537  ax-i9 1541  ax-ial 1545  ax-i5r 1546  ax-ext 2175

This theorem depends on definitions:  df-bi 117  df-nf 1472  df-sb 1774  df-clab 2180  df-cleq 2186  df-clel 2189  df-in 3160  df-ss 3167

This theorem is referenced by:  difdif2ss  3417  difdifdirss  3532  snsstp1  3769  snsstp2  3770  nnregexmid  4654  dmexg  4927  rnexg  4928  ssrnres  5109  cossxp  5189  cocnvss  5192  funinsn  5304  fabexg  5442  foimacnv  5519  ssimaex  5619  oprabss  6005  tposssxp  6304  mapsspw  6740  sbthlemi5  7022  sbthlem7  7024  caserel  7148  dmaddpi  7387  dmmulpi  7388  ltrelxr  8082  nnsscn  8989  nn0sscn  9248  nn0ssq  9696  nnssq  9697  qsscn  9699  fzval2  10080  fzossnn  10259  fzo0ssnn0  10285  expcl2lemap  10625  rpexpcl  10632  expge0  10649  expge1  10650  seq3coll  10916  summodclem2a  11527  fsum3cvg3  11542  fsumrpcl  11550  fsumge0  11605  prodmodclem2a  11722  fprodrpcl  11757  fprodge0  11783  fprodge1  11785  infssuzcldc  12091  nninfctlemfo  12180  isprm3  12259  eulerthlemrprm  12370  eulerthlema  12371  eulerthlemh  12372  eulerthlemth  12373  pcprecl  12430  pcprendvds  12431  pcpremul  12434  4sqlem11  12542  structfn  12640  strleun  12725  cnfldbas  14059  mpocnfldadd  14060  mpocnfldmul  14062  cnfldcj  14064  cnfldtset  14065  cnfldle  14066  cnfldds  14067  psrplusgg  14173  toponsspwpwg  14201  dmtopon  14202  lmbrf  14394  lmres  14427  txcnmpt  14452  qtopbas  14701  tgqioo  14734  dvrecap  14892  cosz12  14956  ioocosf1o  15030  lgsfcl2  15163  2sqlem6  15277  2sqlem8  15280  2sqlem9  15281