Theorem sstri 3236

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

Syntax hints:   ⊆ wss 3200

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 1495  ax-7 1496  ax-gen 1497  ax-ie1 1541  ax-ie2 1542  ax-8 1552  ax-11 1554  ax-4 1558  ax-17 1574  ax-i9 1578  ax-ial 1582  ax-i5r 1583  ax-ext 2213

This theorem depends on definitions:  df-bi 117  df-nf 1509  df-sb 1811  df-clab 2218  df-cleq 2224  df-clel 2227  df-in 3206  df-ss 3213

This theorem is referenced by:  difdif2ss  3464  difdifdirss  3579  snsstp1  3823  snsstp2  3824  elopabran  4378  nnregexmid  4719  dmexg  4996  rnexg  4997  ssrnres  5179  cossxp  5259  cocnvss  5262  funinsn  5379  fabexg  5524  foimacnv  5601  ssimaex  5707  oprabss  6106  tposssxp  6414  mapsspw  6852  sbthlemi5  7159  sbthlem7  7161  caserel  7285  dmaddpi  7544  dmmulpi  7545  ltrelxr  8239  nnsscn  9147  nn0sscn  9406  nn0ssq  9861  nnssq  9862  qsscn  9864  fzval2  10245  fzossnn  10428  fzo0ssnn0  10459  infssuzcldc  10494  expcl2lemap  10812  rpexpcl  10819  expge0  10836  expge1  10837  seq3coll  11105  summodclem2a  11941  fsum3cvg3  11956  fsumrpcl  11964  fsumge0  12019  prodmodclem2a  12136  fprodrpcl  12171  fprodge0  12197  fprodge1  12199  nninfctlemfo  12610  isprm3  12689  eulerthlemrprm  12800  eulerthlema  12801  eulerthlemh  12802  eulerthlemth  12803  pcprecl  12861  pcprendvds  12862  pcpremul  12865  4sqlem11  12973  structfn  13100  strleun  13186  prdsvallem  13354  prdsval  13355  prdssca  13357  prdsbas  13358  prdsplusg  13359  prdsmulr  13360  cnfldbas  14573  mpocnfldadd  14574  mpocnfldmul  14576  cnfldcj  14578  cnfldtset  14579  cnfldle  14580  cnfldds  14581  psrplusgg  14691  toponsspwpwg  14745  dmtopon  14746  lmbrf  14938  lmres  14971  txcnmpt  14996  qtopbas  15245  tgqioo  15278  dvrecap  15436  cosz12  15503  ioocosf1o  15577  mpodvdsmulf1o  15713  fsumdvdsmul  15714  lgsfcl2  15734  2sqlem6  15848  2sqlem8  15851  2sqlem9  15852  trlsex  16237  eupthsg  16295