Theorem sstri 3257

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

Syntax hints:   C_ wss 3220

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 1500  ax-7 1501  ax-gen 1502  ax-ie1 1546  ax-ie2 1547  ax-8 1557  ax-11 1559  ax-4 1563  ax-17 1579  ax-i9 1583  ax-ial 1587  ax-i5r 1588  ax-ext 2220

This theorem depends on definitions:  df-bi 117  df-nf 1514  df-sb 1816  df-clab 2225  df-cleq 2231  df-clel 2234  df-in 3226  df-ss 3233

This theorem is referenced by:  difdif2ss  3488  difdifdirss  3612  snsstp1  3863  snsstp2  3864  elopabran  4424  nnregexmid  4766  dmexg  5044  rnexg  5045  ssrnres  5228  cossxp  5308  cocnvss  5311  funinsn  5428  fabexg  5577  foimacnv  5655  ssimaex  5761  oprabss  6167  tposssxp  6513  mapsspw  6958  sbthlemi5  7271  sbthlem7  7273  caserel  7420  dmaddpi  7685  dmmulpi  7686  ltrelxr  8379  nnsscn  9291  nn0sscn  9550  nn0ssq  10010  nnssq  10011  qsscn  10013  fzval2  10396  fzossnn  10583  fzo0ssnn0  10614  infssuzcldc  10649  expcl2lemap  10969  rpexpcl  10976  expge0  10993  expge1  10994  seq3coll  11275  summodclem2a  12129  fsum3cvg3  12144  fsumrpcl  12152  fsumge0  12207  prodmodclem2a  12324  fprodrpcl  12359  fprodge0  12385  fprodge1  12387  nninfctlemfo  12798  isprm3  12877  eulerthlemrprm  12988  eulerthlema  12989  eulerthlemh  12990  eulerthlemth  12991  pcprecl  13049  pcprendvds  13050  pcpremul  13053  4sqlem11  13161  ballotfilemfc0  13213  ballotfilemfcc  13214  ballotfilemiex  13225  ballotfilemsima  13240  structfn  13352  strleun  13438  prdsvallem  13601  prdsval  14153  prdssca  14155  prdsbas  14156  prdsplusg  14157  prdsmulr  14158  cnfldbas  14872  mpocnfldadd  14873  mpocnfldmul  14875  cnfldcj  14877  cnfldtset  14878  cnfldle  14879  cnfldds  14880  psrplusgg  14995  toponsspwpwg  15049  dmtopon  15050  lmbrf  15242  lmres  15275  txcnmpt  15300  qtopbas  15549  tgqioo  15582  dvrecap  15740  cosz12  15807  ioocosf1o  15881  mpodvdsmulf1o  16021  fsumdvdsmul  16022  lgsfcl2  16042  2sqlem6  16156  2sqlem8  16159  2sqlem9  16160  trlsex  16545  eupthsg  16603