Theorem sstri 3237

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

Syntax hints:   C_ wss 3201

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 1496  ax-7 1497  ax-gen 1498  ax-ie1 1542  ax-ie2 1543  ax-8 1553  ax-11 1555  ax-4 1559  ax-17 1575  ax-i9 1579  ax-ial 1583  ax-i5r 1584  ax-ext 2213

This theorem depends on definitions:  df-bi 117  df-nf 1510  df-sb 1811  df-clab 2218  df-cleq 2224  df-clel 2227  df-in 3207  df-ss 3214

This theorem is referenced by:  difdif2ss  3466  difdifdirss  3581  snsstp1  3828  snsstp2  3829  elopabran  4384  nnregexmid  4725  dmexg  5002  rnexg  5003  ssrnres  5186  cossxp  5266  cocnvss  5269  funinsn  5386  fabexg  5532  foimacnv  5610  ssimaex  5716  oprabss  6117  tposssxp  6458  mapsspw  6896  sbthlemi5  7203  sbthlem7  7205  caserel  7346  dmaddpi  7605  dmmulpi  7606  ltrelxr  8299  nnsscn  9207  nn0sscn  9466  nn0ssq  9923  nnssq  9924  qsscn  9926  fzval2  10308  fzossnn  10492  fzo0ssnn0  10523  infssuzcldc  10558  expcl2lemap  10876  rpexpcl  10883  expge0  10900  expge1  10901  seq3coll  11169  summodclem2a  12022  fsum3cvg3  12037  fsumrpcl  12045  fsumge0  12100  prodmodclem2a  12217  fprodrpcl  12252  fprodge0  12278  fprodge1  12280  nninfctlemfo  12691  isprm3  12770  eulerthlemrprm  12881  eulerthlema  12882  eulerthlemh  12883  eulerthlemth  12884  pcprecl  12942  pcprendvds  12943  pcpremul  12946  4sqlem11  13054  structfn  13181  strleun  13267  prdsvallem  13435  prdsval  13436  prdssca  13438  prdsbas  13439  prdsplusg  13440  prdsmulr  13441  cnfldbas  14656  mpocnfldadd  14657  mpocnfldmul  14659  cnfldcj  14661  cnfldtset  14662  cnfldle  14663  cnfldds  14664  psrplusgg  14779  toponsspwpwg  14833  dmtopon  14834  lmbrf  15026  lmres  15059  txcnmpt  15084  qtopbas  15333  tgqioo  15366  dvrecap  15524  cosz12  15591  ioocosf1o  15665  mpodvdsmulf1o  15804  fsumdvdsmul  15805  lgsfcl2  15825  2sqlem6  15939  2sqlem8  15942  2sqlem9  15943  trlsex  16328  eupthsg  16386