Theorem sstri 3202

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

Syntax hints:   C_ wss 3166

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 1470  ax-7 1471  ax-gen 1472  ax-ie1 1516  ax-ie2 1517  ax-8 1527  ax-11 1529  ax-4 1533  ax-17 1549  ax-i9 1553  ax-ial 1557  ax-i5r 1558  ax-ext 2187

This theorem depends on definitions:  df-bi 117  df-nf 1484  df-sb 1786  df-clab 2192  df-cleq 2198  df-clel 2201  df-in 3172  df-ss 3179

This theorem is referenced by:  difdif2ss  3430  difdifdirss  3545  snsstp1  3783  snsstp2  3784  nnregexmid  4669  dmexg  4942  rnexg  4943  ssrnres  5125  cossxp  5205  cocnvss  5208  funinsn  5323  fabexg  5463  foimacnv  5540  ssimaex  5640  oprabss  6031  tposssxp  6335  mapsspw  6771  sbthlemi5  7063  sbthlem7  7065  caserel  7189  dmaddpi  7438  dmmulpi  7439  ltrelxr  8133  nnsscn  9041  nn0sscn  9300  nn0ssq  9749  nnssq  9750  qsscn  9752  fzval2  10133  fzossnn  10313  fzo0ssnn0  10344  infssuzcldc  10378  expcl2lemap  10696  rpexpcl  10703  expge0  10720  expge1  10721  seq3coll  10987  summodclem2a  11692  fsum3cvg3  11707  fsumrpcl  11715  fsumge0  11770  prodmodclem2a  11887  fprodrpcl  11922  fprodge0  11948  fprodge1  11950  nninfctlemfo  12361  isprm3  12440  eulerthlemrprm  12551  eulerthlema  12552  eulerthlemh  12553  eulerthlemth  12554  pcprecl  12612  pcprendvds  12613  pcpremul  12616  4sqlem11  12724  structfn  12851  strleun  12936  prdsvallem  13104  prdsval  13105  prdssca  13107  prdsbas  13108  prdsplusg  13109  prdsmulr  13110  cnfldbas  14322  mpocnfldadd  14323  mpocnfldmul  14325  cnfldcj  14327  cnfldtset  14328  cnfldle  14329  cnfldds  14330  psrplusgg  14440  toponsspwpwg  14494  dmtopon  14495  lmbrf  14687  lmres  14720  txcnmpt  14745  qtopbas  14994  tgqioo  15027  dvrecap  15185  cosz12  15252  ioocosf1o  15326  mpodvdsmulf1o  15462  fsumdvdsmul  15463  lgsfcl2  15483  2sqlem6  15597  2sqlem8  15600  2sqlem9  15601