Theorem sstri 3257

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

Syntax hints:   ⊆ wss 3220

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 1500  ax-7 1501  ax-gen 1502  ax-ie1 1546  ax-ie2 1547  ax-8 1557  ax-11 1559  ax-4 1563  ax-17 1579  ax-i9 1583  ax-ial 1587  ax-i5r 1588  ax-ext 2220

This theorem depends on definitions:  df-bi 117  df-nf 1514  df-sb 1816  df-clab 2225  df-cleq 2231  df-clel 2234  df-in 3226  df-ss 3233

This theorem is referenced by:  difdif2ss  3488  difdifdirss  3609  snsstp1  3860  snsstp2  3861  elopabran  4421  nnregexmid  4763  dmexg  5041  rnexg  5042  ssrnres  5225  cossxp  5305  cocnvss  5308  funinsn  5425  fabexg  5574  foimacnv  5652  ssimaex  5758  oprabss  6164  tposssxp  6510  mapsspw  6955  sbthlemi5  7268  sbthlem7  7270  caserel  7417  dmaddpi  7682  dmmulpi  7683  ltrelxr  8376  nnsscn  9288  nn0sscn  9547  nn0ssq  10007  nnssq  10008  qsscn  10010  fzval2  10393  fzossnn  10580  fzo0ssnn0  10611  infssuzcldc  10646  expcl2lemap  10966  rpexpcl  10973  expge0  10990  expge1  10991  seq3coll  11272  summodclem2a  12126  fsum3cvg3  12141  fsumrpcl  12149  fsumge0  12204  prodmodclem2a  12321  fprodrpcl  12356  fprodge0  12382  fprodge1  12384  nninfctlemfo  12795  isprm3  12874  eulerthlemrprm  12985  eulerthlema  12986  eulerthlemh  12987  eulerthlemth  12988  pcprecl  13046  pcprendvds  13047  pcpremul  13050  4sqlem11  13158  ballotfilemfc0  13210  ballotfilemfcc  13211  ballotfilemiex  13222  ballotfilemsima  13237  structfn  13349  strleun  13435  prdsvallem  13598  prdsval  14150  prdssca  14152  prdsbas  14153  prdsplusg  14154  prdsmulr  14155  cnfldbas  14869  mpocnfldadd  14870  mpocnfldmul  14872  cnfldcj  14874  cnfldtset  14875  cnfldle  14876  cnfldds  14877  psrplusgg  14992  toponsspwpwg  15046  dmtopon  15047  lmbrf  15239  lmres  15272  txcnmpt  15297  qtopbas  15546  tgqioo  15579  dvrecap  15737  cosz12  15804  ioocosf1o  15878  mpodvdsmulf1o  16018  fsumdvdsmul  16019  lgsfcl2  16039  2sqlem6  16153  2sqlem8  16156  2sqlem9  16157  trlsex  16542  eupthsg  16600