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  5580  oprabss  5964  tposssxp  6253  mapsspw  6687  sbthlemi5  6963  sbthlem7  6965  caserel  7089  dmaddpi  7327  dmmulpi  7328  ltrelxr  8021  nnsscn  8927  nn0sscn  9184  nn0ssq  9631  nnssq  9632  qsscn  9634  fzval2  10014  fzossnn  10192  fzo0ssnn0  10218  expcl2lemap  10535  rpexpcl  10542  expge0  10559  expge1  10560  seq3coll  10825  summodclem2a  11392  fsum3cvg3  11407  fsumrpcl  11415  fsumge0  11470  prodmodclem2a  11587  fprodrpcl  11622  fprodge0  11648  fprodge1  11650  infssuzcldc  11955  isprm3  12121  eulerthlemrprm  12232  eulerthlema  12233  eulerthlemh  12234  eulerthlemth  12235  pcprecl  12292  pcprendvds  12293  pcpremul  12296  structfn  12484  strleun  12566  cnfldbas  13599  cnfldadd  13600  cnfldmul  13601  toponsspwpwg  13662  dmtopon  13663  lmbrf  13855  lmres  13888  txcnmpt  13913  qtopbas  14162  tgqioo  14187  dvrecap  14317  cosz12  14341  ioocosf1o  14415  lgsfcl2  14547  2sqlem6  14607  2sqlem8  14610  2sqlem9  14611