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  4670  dmexg  4943  rnexg  4944  ssrnres  5126  cossxp  5206  cocnvss  5209  funinsn  5324  fabexg  5465  foimacnv  5542  ssimaex  5642  oprabss  6033  tposssxp  6337  mapsspw  6773  sbthlemi5  7065  sbthlem7  7067  caserel  7191  dmaddpi  7440  dmmulpi  7441  ltrelxr  8135  nnsscn  9043  nn0sscn  9302  nn0ssq  9751  nnssq  9752  qsscn  9754  fzval2  10135  fzossnn  10315  fzo0ssnn0  10346  infssuzcldc  10380  expcl2lemap  10698  rpexpcl  10705  expge0  10722  expge1  10723  seq3coll  10989  summodclem2a  11725  fsum3cvg3  11740  fsumrpcl  11748  fsumge0  11803  prodmodclem2a  11920  fprodrpcl  11955  fprodge0  11981  fprodge1  11983  nninfctlemfo  12394  isprm3  12473  eulerthlemrprm  12584  eulerthlema  12585  eulerthlemh  12586  eulerthlemth  12587  pcprecl  12645  pcprendvds  12646  pcpremul  12649  4sqlem11  12757  structfn  12884  strleun  12969  prdsvallem  13137  prdsval  13138  prdssca  13140  prdsbas  13141  prdsplusg  13142  prdsmulr  13143  cnfldbas  14355  mpocnfldadd  14356  mpocnfldmul  14358  cnfldcj  14360  cnfldtset  14361  cnfldle  14362  cnfldds  14363  psrplusgg  14473  toponsspwpwg  14527  dmtopon  14528  lmbrf  14720  lmres  14753  txcnmpt  14778  qtopbas  15027  tgqioo  15060  dvrecap  15218  cosz12  15285  ioocosf1o  15359  mpodvdsmulf1o  15495  fsumdvdsmul  15496  lgsfcl2  15516  2sqlem6  15630  2sqlem8  15633  2sqlem9  15634