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  5515  foimacnv  5592  ssimaex  5697  oprabss  6096  tposssxp  6401  mapsspw  6839  sbthlemi5  7139  sbthlem7  7141  caserel  7265  dmaddpi  7523  dmmulpi  7524  ltrelxr  8218  nnsscn  9126  nn0sscn  9385  nn0ssq  9835  nnssq  9836  qsscn  9838  fzval2  10219  fzossnn  10402  fzo0ssnn0  10433  infssuzcldc  10467  expcl2lemap  10785  rpexpcl  10792  expge0  10809  expge1  10810  seq3coll  11077  summodclem2a  11908  fsum3cvg3  11923  fsumrpcl  11931  fsumge0  11986  prodmodclem2a  12103  fprodrpcl  12138  fprodge0  12164  fprodge1  12166  nninfctlemfo  12577  isprm3  12656  eulerthlemrprm  12767  eulerthlema  12768  eulerthlemh  12769  eulerthlemth  12770  pcprecl  12828  pcprendvds  12829  pcpremul  12832  4sqlem11  12940  structfn  13067  strleun  13153  prdsvallem  13321  prdsval  13322  prdssca  13324  prdsbas  13325  prdsplusg  13326  prdsmulr  13327  cnfldbas  14540  mpocnfldadd  14541  mpocnfldmul  14543  cnfldcj  14545  cnfldtset  14546  cnfldle  14547  cnfldds  14548  psrplusgg  14658  toponsspwpwg  14712  dmtopon  14713  lmbrf  14905  lmres  14938  txcnmpt  14963  qtopbas  15212  tgqioo  15245  dvrecap  15403  cosz12  15470  ioocosf1o  15544  mpodvdsmulf1o  15680  fsumdvdsmul  15681  lgsfcl2  15701  2sqlem6  15815  2sqlem8  15818  2sqlem9  15819