Theorem sstri 3111

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 3109	. 2 |- ( A C_ B -> ( B C_ C -> A C_ C ) )
4	1, 2, 3	mp2 16	1 |- A C_ C

Syntax hints:   C_ wss 3076

This theorem was proved from axioms:  ax-mp 5  ax-1 6  ax-2 7  ax-ia1 105  ax-ia2 106  ax-ia3 107  ax-5 1424  ax-7 1425  ax-gen 1426  ax-ie1 1470  ax-ie2 1471  ax-8 1483  ax-11 1485  ax-4 1488  ax-17 1507  ax-i9 1511  ax-ial 1515  ax-i5r 1516  ax-ext 2122

This theorem depends on definitions:  df-bi 116  df-nf 1438  df-sb 1737  df-clab 2127  df-cleq 2133  df-clel 2136  df-in 3082  df-ss 3089

This theorem is referenced by:  difdif2ss  3338  difdifdirss  3452  snsstp1  3678  snsstp2  3679  nnregexmid  4542  dmexg  4811  rnexg  4812  ssrnres  4989  cossxp  5069  cocnvss  5072  funinsn  5180  fabexg  5318  foimacnv  5393  ssimaex  5490  oprabss  5865  tposssxp  6154  mapsspw  6586  sbthlemi5  6857  sbthlem7  6859  caserel  6980  dmaddpi  7157  dmmulpi  7158  ltrelxr  7849  nnsscn  8749  nn0sscn  9006  nn0ssq  9447  nnssq  9448  qsscn  9450  fzval2  9824  fzossnn  9997  fzo0ssnn0  10023  expcl2lemap  10336  rpexpcl  10343  expge0  10360  expge1  10361  seq3coll  10617  summodclem2a  11182  fsum3cvg3  11197  fsumrpcl  11205  fsumge0  11260  prodmodclem2a  11377  infssuzcldc  11680  isprm3  11835  structfn  12017  strleun  12087  toponsspwpwg  12228  dmtopon  12229  lmbrf  12423  lmres  12456  txcnmpt  12481  qtopbas  12730  tgqioo  12755  dvrecap  12885  cosz12  12909  ioocosf1o  12983