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  7411  dmmulpi  7412  ltrelxr  8106  nnsscn  9014  nn0sscn  9273  nn0ssq  9721  nnssq  9722  qsscn  9724  fzval2  10105  fzossnn  10284  fzo0ssnn0  10310  infssuzcldc  10344  expcl2lemap  10662  rpexpcl  10669  expge0  10686  expge1  10687  seq3coll  10953  summodclem2a  11565  fsum3cvg3  11580  fsumrpcl  11588  fsumge0  11643  prodmodclem2a  11760  fprodrpcl  11795  fprodge0  11821  fprodge1  11823  nninfctlemfo  12234  isprm3  12313  eulerthlemrprm  12424  eulerthlema  12425  eulerthlemh  12426  eulerthlemth  12427  pcprecl  12485  pcprendvds  12486  pcpremul  12489  4sqlem11  12597  structfn  12724  strleun  12809  prdsvallem  12976  prdsval  12977  prdssca  12979  prdsbas  12980  prdsplusg  12981  prdsmulr  12982  cnfldbas  14194  mpocnfldadd  14195  mpocnfldmul  14197  cnfldcj  14199  cnfldtset  14200  cnfldle  14201  cnfldds  14202  psrplusgg  14312  toponsspwpwg  14366  dmtopon  14367  lmbrf  14559  lmres  14592  txcnmpt  14617  qtopbas  14866  tgqioo  14899  dvrecap  15057  cosz12  15124  ioocosf1o  15198  mpodvdsmulf1o  15334  fsumdvdsmul  15335  lgsfcl2  15355  2sqlem6  15469  2sqlem8  15472  2sqlem9  15473