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  7428  dmaddpi  7693  dmmulpi  7694  ltrelxr  8387  nnsscn  9312  nn0sscn  9573  nn0ssq  10038  nnssq  10039  qsscn  10041  fzval2  10425  fzossnn  10613  fzo0ssnn0  10644  infssuzcldc  10679  expcl2lemap  11003  rpexpcl  11010  expge0  11027  expge1  11028  seq3coll  11310  summodclem2a  12167  fsum3cvg3  12182  fsumrpcl  12190  fsumge0  12245  prodmodclem2a  12362  fprodrpcl  12397  fprodge0  12423  fprodge1  12425  nninfctlemfo  12836  isprm3  12915  eulerthlemrprm  13030  eulerthlema  13031  eulerthlemh  13032  eulerthlemth  13033  pcprecl  13091  pcprendvds  13092  pcpremul  13095  4sqlem11  13203  ballotfilemfc0  13284  ballotfilemfcc  13285  ballotfilemiex  13296  ballotfilemsima  13311  structfn  13423  strleun  13511  prdsvallem  13674  prdsval  14257  prdssca  14259  prdsbas  14260  prdsplusg  14261  prdsmulr  14262  cnfldbas  14981  mpocnfldadd  14982  mpocnfldmul  14984  cnfldcj  14986  cnfldtset  14987  cnfldle  14988  cnfldds  14989  asplss  15100  aspsubrg  15102  psrplusgg  15154  psrmulrg  15158  toponsspwpwg  15214  dmtopon  15215  lmbrf  15407  lmres  15440  txcnmpt  15465  qtopbas  15714  tgqioo  15747  dvrecap  15905  cosz12  15973  ioocosf1o  16047  efnnfsumcl  16200  efchtqdvds  16226  mpodvdsmulf1o  16245  fsumdvdsmul  16246  lgsfcl2  16291  2sqlem6  16405  2sqlem8  16408  2sqlem9  16409  trlsex  16794  eupthsg  16852