Theorem sstri 3164

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

Syntax hints:   C_ wss 3129

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 1447  ax-7 1448  ax-gen 1449  ax-ie1 1493  ax-ie2 1494  ax-8 1504  ax-11 1506  ax-4 1510  ax-17 1526  ax-i9 1530  ax-ial 1534  ax-i5r 1535  ax-ext 2159

This theorem depends on definitions:  df-bi 117  df-nf 1461  df-sb 1763  df-clab 2164  df-cleq 2170  df-clel 2173  df-in 3135  df-ss 3142

This theorem is referenced by:  difdif2ss  3392  difdifdirss  3507  snsstp1  3742  snsstp2  3743  nnregexmid  4620  dmexg  4891  rnexg  4892  ssrnres  5071  cossxp  5151  cocnvss  5154  funinsn  5265  fabexg  5403  foimacnv  5479  ssimaex  5577  oprabss  5960  tposssxp  6249  mapsspw  6683  sbthlemi5  6959  sbthlem7  6961  caserel  7085  dmaddpi  7323  dmmulpi  7324  ltrelxr  8017  nnsscn  8923  nn0sscn  9180  nn0ssq  9627  nnssq  9628  qsscn  9630  fzval2  10010  fzossnn  10188  fzo0ssnn0  10214  expcl2lemap  10531  rpexpcl  10538  expge0  10555  expge1  10556  seq3coll  10821  summodclem2a  11388  fsum3cvg3  11403  fsumrpcl  11411  fsumge0  11466  prodmodclem2a  11583  fprodrpcl  11618  fprodge0  11644  fprodge1  11646  infssuzcldc  11951  isprm3  12117  eulerthlemrprm  12228  eulerthlema  12229  eulerthlemh  12230  eulerthlemth  12231  pcprecl  12288  pcprendvds  12289  pcpremul  12292  structfn  12480  strleun  12562  cnfldbas  13429  cnfldadd  13430  cnfldmul  13431  toponsspwpwg  13492  dmtopon  13493  lmbrf  13685  lmres  13718  txcnmpt  13743  qtopbas  13992  tgqioo  14017  dvrecap  14147  cosz12  14171  ioocosf1o  14245  lgsfcl2  14377  2sqlem6  14437  2sqlem8  14440  2sqlem9  14441