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  4428  nnregexmid  4770  dmexg  5048  rnexg  5049  ssrnres  5233  cossxp  5313  cocnvss  5316  funinsn  5433  fabexg  5582  foimacnv  5660  ssimaex  5767  oprabss  6177  tposssxp  6525  mapsspw  6970  sbthlemi5  7285  sbthlem7  7287  caserel  7433  dmaddpi  7698  dmmulpi  7699  ltrelxr  8392  nnsscn  9318  nn0sscn  9579  nn0ssq  10043  nnssq  10044  qsscn  10046  fzval2  10430  fzossnn  10618  fzo0ssnn0  10649  infssuzcldc  10684  expcl2lemap  11008  rpexpcl  11015  expge0  11032  expge1  11033  seq3coll  11315  summodclem2a  12172  fsum3cvg3  12187  fsumrpcl  12195  fsumge0  12250  prodmodclem2a  12367  fprodrpcl  12402  fprodge0  12428  fprodge1  12430  nninfctlemfo  12841  isprm3  12920  eulerthlemrprm  13035  eulerthlema  13036  eulerthlemh  13037  eulerthlemth  13038  pcprecl  13096  pcprendvds  13097  pcpremul  13100  4sqlem11  13208  ballotfilemfc0  13289  ballotfilemfcc  13290  ballotfilemiex  13301  ballotfilemsima  13316  structfn  13428  strleun  13516  prdsvallem  13679  prdsval  14279  prdssca  14281  prdsbas  14282  prdsplusg  14283  prdsmulr  14284  cnfldbas  15005  mpocnfldadd  15006  mpocnfldmul  15008  cnfldcj  15010  cnfldtset  15011  cnfldle  15012  cnfldds  15013  asplss  15124  aspsubrg  15126  psrplusgg  15191  psrmulrg  15195  toponsspwpwg  15265  dmtopon  15266  lmbrf  15458  lmres  15491  txcnmpt  15516  qtopbas  15765  tgqioo  15798  dvrecap  15956  cosz12  16024  ioocosf1o  16099  efnnfsumcl  16256  efchtqdvds  16282  mpodvdsmulf1o  16301  fsumdvdsmul  16302  lgsfcl2  16347  2sqlem6  16461  2sqlem8  16464  2sqlem9  16465  trlsex  16850  eupthsg  16908