Theorem sstri 3156

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

Syntax hints:   C_ wss 3121

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 1440  ax-7 1441  ax-gen 1442  ax-ie1 1486  ax-ie2 1487  ax-8 1497  ax-11 1499  ax-4 1503  ax-17 1519  ax-i9 1523  ax-ial 1527  ax-i5r 1528  ax-ext 2152

This theorem depends on definitions:  df-bi 116  df-nf 1454  df-sb 1756  df-clab 2157  df-cleq 2163  df-clel 2166  df-in 3127  df-ss 3134

This theorem is referenced by:  difdif2ss  3384  difdifdirss  3499  snsstp1  3730  snsstp2  3731  nnregexmid  4605  dmexg  4875  rnexg  4876  ssrnres  5053  cossxp  5133  cocnvss  5136  funinsn  5247  fabexg  5385  foimacnv  5460  ssimaex  5557  oprabss  5939  tposssxp  6228  mapsspw  6662  sbthlemi5  6938  sbthlem7  6940  caserel  7064  dmaddpi  7287  dmmulpi  7288  ltrelxr  7980  nnsscn  8883  nn0sscn  9140  nn0ssq  9587  nnssq  9588  qsscn  9590  fzval2  9968  fzossnn  10145  fzo0ssnn0  10171  expcl2lemap  10488  rpexpcl  10495  expge0  10512  expge1  10513  seq3coll  10777  summodclem2a  11344  fsum3cvg3  11359  fsumrpcl  11367  fsumge0  11422  prodmodclem2a  11539  fprodrpcl  11574  fprodge0  11600  fprodge1  11602  infssuzcldc  11906  isprm3  12072  eulerthlemrprm  12183  eulerthlema  12184  eulerthlemh  12185  eulerthlemth  12186  pcprecl  12243  pcprendvds  12244  pcpremul  12247  structfn  12435  strleun  12507  toponsspwpwg  12814  dmtopon  12815  lmbrf  13009  lmres  13042  txcnmpt  13067  qtopbas  13316  tgqioo  13341  dvrecap  13471  cosz12  13495  ioocosf1o  13569  lgsfcl2  13701  2sqlem6  13750  2sqlem8  13753  2sqlem9  13754