Theorem sstri 3233

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

Syntax hints:   C_ wss 3197

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 1493  ax-7 1494  ax-gen 1495  ax-ie1 1539  ax-ie2 1540  ax-8 1550  ax-11 1552  ax-4 1556  ax-17 1572  ax-i9 1576  ax-ial 1580  ax-i5r 1581  ax-ext 2211

This theorem depends on definitions:  df-bi 117  df-nf 1507  df-sb 1809  df-clab 2216  df-cleq 2222  df-clel 2225  df-in 3203  df-ss 3210

This theorem is referenced by:  difdif2ss  3461  difdifdirss  3576  snsstp1  3818  snsstp2  3819  elopabran  4372  nnregexmid  4713  dmexg  4988  rnexg  4989  ssrnres  5171  cossxp  5251  cocnvss  5254  funinsn  5370  fabexg  5513  foimacnv  5590  ssimaex  5695  oprabss  6090  tposssxp  6395  mapsspw  6831  sbthlemi5  7128  sbthlem7  7130  caserel  7254  dmaddpi  7512  dmmulpi  7513  ltrelxr  8207  nnsscn  9115  nn0sscn  9374  nn0ssq  9823  nnssq  9824  qsscn  9826  fzval2  10207  fzossnn  10390  fzo0ssnn0  10421  infssuzcldc  10455  expcl2lemap  10773  rpexpcl  10780  expge0  10797  expge1  10798  seq3coll  11064  summodclem2a  11892  fsum3cvg3  11907  fsumrpcl  11915  fsumge0  11970  prodmodclem2a  12087  fprodrpcl  12122  fprodge0  12148  fprodge1  12150  nninfctlemfo  12561  isprm3  12640  eulerthlemrprm  12751  eulerthlema  12752  eulerthlemh  12753  eulerthlemth  12754  pcprecl  12812  pcprendvds  12813  pcpremul  12816  4sqlem11  12924  structfn  13051  strleun  13137  prdsvallem  13305  prdsval  13306  prdssca  13308  prdsbas  13309  prdsplusg  13310  prdsmulr  13311  cnfldbas  14524  mpocnfldadd  14525  mpocnfldmul  14527  cnfldcj  14529  cnfldtset  14530  cnfldle  14531  cnfldds  14532  psrplusgg  14642  toponsspwpwg  14696  dmtopon  14697  lmbrf  14889  lmres  14922  txcnmpt  14947  qtopbas  15196  tgqioo  15229  dvrecap  15387  cosz12  15454  ioocosf1o  15528  mpodvdsmulf1o  15664  fsumdvdsmul  15665  lgsfcl2  15685  2sqlem6  15799  2sqlem8  15802  2sqlem9  15803