Theorem sstri 3210

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

Syntax hints:   C_ wss 3174

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 1471  ax-7 1472  ax-gen 1473  ax-ie1 1517  ax-ie2 1518  ax-8 1528  ax-11 1530  ax-4 1534  ax-17 1550  ax-i9 1554  ax-ial 1558  ax-i5r 1559  ax-ext 2189

This theorem depends on definitions:  df-bi 117  df-nf 1485  df-sb 1787  df-clab 2194  df-cleq 2200  df-clel 2203  df-in 3180  df-ss 3187

This theorem is referenced by:  difdif2ss  3438  difdifdirss  3553  snsstp1  3794  snsstp2  3795  nnregexmid  4687  dmexg  4961  rnexg  4962  ssrnres  5144  cossxp  5224  cocnvss  5227  funinsn  5342  fabexg  5485  foimacnv  5562  ssimaex  5663  oprabss  6054  tposssxp  6358  mapsspw  6794  sbthlemi5  7089  sbthlem7  7091  caserel  7215  dmaddpi  7473  dmmulpi  7474  ltrelxr  8168  nnsscn  9076  nn0sscn  9335  nn0ssq  9784  nnssq  9785  qsscn  9787  fzval2  10168  fzossnn  10350  fzo0ssnn0  10381  infssuzcldc  10415  expcl2lemap  10733  rpexpcl  10740  expge0  10757  expge1  10758  seq3coll  11024  summodclem2a  11807  fsum3cvg3  11822  fsumrpcl  11830  fsumge0  11885  prodmodclem2a  12002  fprodrpcl  12037  fprodge0  12063  fprodge1  12065  nninfctlemfo  12476  isprm3  12555  eulerthlemrprm  12666  eulerthlema  12667  eulerthlemh  12668  eulerthlemth  12669  pcprecl  12727  pcprendvds  12728  pcpremul  12731  4sqlem11  12839  structfn  12966  strleun  13051  prdsvallem  13219  prdsval  13220  prdssca  13222  prdsbas  13223  prdsplusg  13224  prdsmulr  13225  cnfldbas  14437  mpocnfldadd  14438  mpocnfldmul  14440  cnfldcj  14442  cnfldtset  14443  cnfldle  14444  cnfldds  14445  psrplusgg  14555  toponsspwpwg  14609  dmtopon  14610  lmbrf  14802  lmres  14835  txcnmpt  14860  qtopbas  15109  tgqioo  15142  dvrecap  15300  cosz12  15367  ioocosf1o  15441  mpodvdsmulf1o  15577  fsumdvdsmul  15578  lgsfcl2  15598  2sqlem6  15712  2sqlem8  15715  2sqlem9  15716