Theorem sstri 3166

Description: Subclass transitivity inference. (Contributed by NM, 5-May-2000.)

Hypotheses

Ref	Expression
sstri.1	|- A C_ B
sstri.2	|- B C_ C

Assertion

Ref	Expression
sstri	|- A C_ C

Proof of Theorem sstri

Step	Hyp	Ref	Expression
1		sstri.1	. 2 |- A C_ B
2		sstri.2	. 2 |- B C_ C
3		sstr2 3164	. 2 |- ( A C_ B -> ( B C_ C -> A C_ C ) )
4	1, 2, 3	mp2 16	1 |- A C_ C

Syntax hints:   C_ wss 3131

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 1447  ax-7 1448  ax-gen 1449  ax-ie1 1493  ax-ie2 1494  ax-8 1504  ax-11 1506  ax-4 1510  ax-17 1526  ax-i9 1530  ax-ial 1534  ax-i5r 1535  ax-ext 2159

This theorem depends on definitions:  df-bi 117  df-nf 1461  df-sb 1763  df-clab 2164  df-cleq 2170  df-clel 2173  df-in 3137  df-ss 3144

This theorem is referenced by:  difdif2ss  3394  difdifdirss  3509  snsstp1  3744  snsstp2  3745  nnregexmid  4622  dmexg  4893  rnexg  4894  ssrnres  5073  cossxp  5153  cocnvss  5156  funinsn  5267  fabexg  5405  foimacnv  5481  ssimaex  5579  oprabss  5963  tposssxp  6252  mapsspw  6686  sbthlemi5  6962  sbthlem7  6964  caserel  7088  dmaddpi  7326  dmmulpi  7327  ltrelxr  8020  nnsscn  8926  nn0sscn  9183  nn0ssq  9630  nnssq  9631  qsscn  9633  fzval2  10013  fzossnn  10191  fzo0ssnn0  10217  expcl2lemap  10534  rpexpcl  10541  expge0  10558  expge1  10559  seq3coll  10824  summodclem2a  11391  fsum3cvg3  11406  fsumrpcl  11414  fsumge0  11469  prodmodclem2a  11586  fprodrpcl  11621  fprodge0  11647  fprodge1  11649  infssuzcldc  11954  isprm3  12120  eulerthlemrprm  12231  eulerthlema  12232  eulerthlemh  12233  eulerthlemth  12234  pcprecl  12291  pcprendvds  12292  pcpremul  12295  structfn  12483  strleun  12565  cnfldbas  13498  cnfldadd  13499  cnfldmul  13500  toponsspwpwg  13561  dmtopon  13562  lmbrf  13754  lmres  13787  txcnmpt  13812  qtopbas  14061  tgqioo  14086  dvrecap  14216  cosz12  14240  ioocosf1o  14314  lgsfcl2  14446  2sqlem6  14506  2sqlem8  14509  2sqlem9  14510