Theorem sstri 3249

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

Syntax hints:   C_ wss 3213

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 2216

This theorem depends on definitions:  df-bi 117  df-nf 1510  df-sb 1812  df-clab 2221  df-cleq 2227  df-clel 2230  df-in 3219  df-ss 3226

This theorem is referenced by:  difdif2ss  3480  difdifdirss  3596  snsstp1  3846  snsstp2  3847  elopabran  4404  nnregexmid  4745  dmexg  5023  rnexg  5024  ssrnres  5207  cossxp  5287  cocnvss  5290  funinsn  5407  fabexg  5556  foimacnv  5634  ssimaex  5740  oprabss  6141  tposssxp  6482  mapsspw  6920  sbthlemi5  7233  sbthlem7  7235  caserel  7380  dmaddpi  7642  dmmulpi  7643  ltrelxr  8336  nnsscn  9244  nn0sscn  9503  nn0ssq  9963  nnssq  9964  qsscn  9966  fzval2  10348  fzossnn  10533  fzo0ssnn0  10564  infssuzcldc  10599  expcl2lemap  10917  rpexpcl  10924  expge0  10941  expge1  10942  seq3coll  11218  summodclem2a  12071  fsum3cvg3  12086  fsumrpcl  12094  fsumge0  12149  prodmodclem2a  12266  fprodrpcl  12301  fprodge0  12327  fprodge1  12329  nninfctlemfo  12740  isprm3  12819  eulerthlemrprm  12930  eulerthlema  12931  eulerthlemh  12932  eulerthlemth  12933  pcprecl  12991  pcprendvds  12992  pcpremul  12995  4sqlem11  13103  ballotfilemfc0  13153  ballotfilemfcc  13154  structfn  13248  strleun  13334  prdsvallem  13502  prdsval  13503  prdssca  13505  prdsbas  13506  prdsplusg  13507  prdsmulr  13508  cnfldbas  14725  mpocnfldadd  14726  mpocnfldmul  14728  cnfldcj  14730  cnfldtset  14731  cnfldle  14732  cnfldds  14733  psrplusgg  14850  toponsspwpwg  14904  dmtopon  14905  lmbrf  15097  lmres  15130  txcnmpt  15155  qtopbas  15404  tgqioo  15437  dvrecap  15595  cosz12  15662  ioocosf1o  15736  mpodvdsmulf1o  15875  fsumdvdsmul  15876  lgsfcl2  15896  2sqlem6  16010  2sqlem8  16013  2sqlem9  16014  trlsex  16399  eupthsg  16457