Theorem sstri 3188

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

Syntax hints:   C_ wss 3153

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 1458  ax-7 1459  ax-gen 1460  ax-ie1 1504  ax-ie2 1505  ax-8 1515  ax-11 1517  ax-4 1521  ax-17 1537  ax-i9 1541  ax-ial 1545  ax-i5r 1546  ax-ext 2175

This theorem depends on definitions:  df-bi 117  df-nf 1472  df-sb 1774  df-clab 2180  df-cleq 2186  df-clel 2189  df-in 3159  df-ss 3166

This theorem is referenced by:  difdif2ss  3416  difdifdirss  3531  snsstp1  3768  snsstp2  3769  nnregexmid  4653  dmexg  4926  rnexg  4927  ssrnres  5108  cossxp  5188  cocnvss  5191  funinsn  5303  fabexg  5441  foimacnv  5518  ssimaex  5618  oprabss  6004  tposssxp  6302  mapsspw  6738  sbthlemi5  7020  sbthlem7  7022  caserel  7146  dmaddpi  7385  dmmulpi  7386  ltrelxr  8080  nnsscn  8987  nn0sscn  9245  nn0ssq  9693  nnssq  9694  qsscn  9696  fzval2  10077  fzossnn  10256  fzo0ssnn0  10282  expcl2lemap  10622  rpexpcl  10629  expge0  10646  expge1  10647  seq3coll  10913  summodclem2a  11524  fsum3cvg3  11539  fsumrpcl  11547  fsumge0  11602  prodmodclem2a  11719  fprodrpcl  11754  fprodge0  11780  fprodge1  11782  infssuzcldc  12088  nninfctlemfo  12177  isprm3  12256  eulerthlemrprm  12367  eulerthlema  12368  eulerthlemh  12369  eulerthlemth  12370  pcprecl  12427  pcprendvds  12428  pcpremul  12431  4sqlem11  12539  structfn  12637  strleun  12722  cnfldbas  14051  cnfldadd  14052  cnfldmul  14054  psrplusgg  14162  toponsspwpwg  14190  dmtopon  14191  lmbrf  14383  lmres  14416  txcnmpt  14441  qtopbas  14690  tgqioo  14715  dvrecap  14862  cosz12  14915  ioocosf1o  14989  lgsfcl2  15122  2sqlem6  15207  2sqlem8  15210  2sqlem9  15211