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  9311  nn0sscn  9572  nn0ssq  10037  nnssq  10038  qsscn  10040  fzval2  10424  fzossnn  10612  fzo0ssnn0  10643  infssuzcldc  10678  expcl2lemap  11001  rpexpcl  11008  expge0  11025  expge1  11026  seq3coll  11308  summodclem2a  12164  fsum3cvg3  12179  fsumrpcl  12187  fsumge0  12242  prodmodclem2a  12359  fprodrpcl  12394  fprodge0  12420  fprodge1  12422  nninfctlemfo  12833  isprm3  12912  eulerthlemrprm  13027  eulerthlema  13028  eulerthlemh  13029  eulerthlemth  13030  pcprecl  13088  pcprendvds  13089  pcpremul  13092  4sqlem11  13200  ballotfilemfc0  13281  ballotfilemfcc  13282  ballotfilemiex  13293  ballotfilemsima  13308  structfn  13420  strleun  13507  prdsvallem  13670  prdsval  14222  prdssca  14224  prdsbas  14225  prdsplusg  14226  prdsmulr  14227  cnfldbas  14946  mpocnfldadd  14947  mpocnfldmul  14949  cnfldcj  14951  cnfldtset  14952  cnfldle  14953  cnfldds  14954  asplss  15065  aspsubrg  15067  psrplusgg  15118  toponsspwpwg  15172  dmtopon  15173  lmbrf  15365  lmres  15398  txcnmpt  15423  qtopbas  15672  tgqioo  15705  dvrecap  15863  cosz12  15931  ioocosf1o  16005  mpodvdsmulf1o  16185  fsumdvdsmul  16186  lgsfcl2  16223  2sqlem6  16337  2sqlem8  16340  2sqlem9  16341  trlsex  16726  eupthsg  16784