Theorem sstri 3257

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

This proof depends on syntax axioms:   C_ wss 3220

This proof depends on axioms:  ax-mp 5  ax-1 6  ax-2 7  ax-ia1 106  ax-ia2 107  ax-ia3 108  ax-5 1500  ax-7 1501  ax-gen 1502  ax-ie1 1546  ax-ie2 1547  ax-8 1557  ax-11 1559  ax-4 1563  ax-17 1579  ax-i9 1583  ax-ial 1587  ax-i5r 1588  ax-ext 2220

This proof depends on definitions:  df-bi 117  df-nf 1514  df-sb 1816  df-clab 2225  df-cleq 2231  df-clel 2234  df-in 3226  df-ss 3233

This theorem is used by:  difdif2ss  3488  difdifdirss  3612  snsstp1  3865  snsstp2  3866  elopabran  4426  nnregexmid  4768  dmexg  5046  rnexg  5047  ssrnres  5230  cossxp  5310  cocnvss  5313  funinsn  5430  fabexg  5579  foimacnv  5657  ssimaex  5764  oprabss  6174  tposssxp  6520  mapsspw  6965  sbthlemi5  7278  sbthlem7  7280  caserel  7427  dmaddpi  7692  dmmulpi  7693  ltrelxr  8386  nnsscn  9309  nn0sscn  9568  nn0ssq  10028  nnssq  10029  qsscn  10031  fzval2  10414  fzossnn  10602  fzo0ssnn0  10633  infssuzcldc  10668  expcl2lemap  10988  rpexpcl  10995  expge0  11012  expge1  11013  seq3coll  11294  summodclem2a  12148  fsum3cvg3  12163  fsumrpcl  12171  fsumge0  12226  prodmodclem2a  12343  fprodrpcl  12378  fprodge0  12404  fprodge1  12406  nninfctlemfo  12817  isprm3  12896  eulerthlemrprm  13007  eulerthlema  13008  eulerthlemh  13009  eulerthlemth  13010  pcprecl  13068  pcprendvds  13069  pcpremul  13072  4sqlem11  13180  ballotfilemfc0  13232  ballotfilemfcc  13233  ballotfilemiex  13244  ballotfilemsima  13259  structfn  13371  strleun  13458  prdsvallem  13621  prdsval  14173  prdssca  14175  prdsbas  14176  prdsplusg  14177  prdsmulr  14178  cnfldbas  14897  mpocnfldadd  14898  mpocnfldmul  14900  cnfldcj  14902  cnfldtset  14903  cnfldle  14904  cnfldds  14905  asplss  15016  aspsubrg  15018  psrplusgg  15069  toponsspwpwg  15123  dmtopon  15124  lmbrf  15316  lmres  15349  txcnmpt  15374  qtopbas  15623  tgqioo  15656  dvrecap  15814  cosz12  15881  ioocosf1o  15955  mpodvdsmulf1o  16104  fsumdvdsmul  16105  lgsfcl2  16125  2sqlem6  16239  2sqlem8  16242  2sqlem9  16243  trlsex  16628  eupthsg  16686