Theorem sstrid 3108

Description: Subclass transitivity deduction. (Contributed by NM, 6-Feb-2014.)

Hypotheses

Ref	Expression
sstrid.1	|- A C_ B
sstrid.2	|- ( ph -> B C_ C )

Assertion

Ref	Expression
sstrid	|- ( ph -> A C_ C )

Proof of Theorem sstrid

Step	Hyp	Ref	Expression
1		sstrid.1	. . 3 |- A C_ B
2	1	a1i 9	. 2 |- ( ph -> A C_ B )
3		sstrid.2	. 2 |- ( ph -> B C_ C )
4	2, 3	sstrd 3107	1 |- ( ph -> A C_ C )

Syntax hints:   -> wi 4   C_ wss 3071

This theorem was proved from axioms:  ax-mp 5  ax-1 6  ax-2 7  ax-ia1 105  ax-ia2 106  ax-ia3 107  ax-5 1423  ax-7 1424  ax-gen 1425  ax-ie1 1469  ax-ie2 1470  ax-8 1482  ax-11 1484  ax-4 1487  ax-17 1506  ax-i9 1510  ax-ial 1514  ax-i5r 1515  ax-ext 2121

This theorem depends on definitions:  df-bi 116  df-nf 1437  df-sb 1736  df-clab 2126  df-cleq 2132  df-clel 2135  df-in 3077  df-ss 3084

This theorem is referenced by:  cossxp2  5062  fimacnv  5549  smores2  6191  f1imaen2g  6687  phplem4dom  6756  isinfinf  6791  fidcenumlemrk  6842  casef  6973  genipv  7322  fzossnn0  9957  seq3split  10257  ctinf  11948  tgcl  12238  epttop  12264  ntrin  12298  cnconst2  12407  cnrest2  12410  cnptopresti  12412  cnptoprest2  12414  hmeores  12489  blin2  12606  ivthdec  12796  limcdifap  12805  limcresi  12809  dvfgg  12831  dvcnp2cntop  12837  dvaddxxbr  12839