Theorem sstrid 3158

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 3157	1 |- ( ph -> A C_ C )

Syntax hints:   -> wi 4   C_ wss 3121

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 1440  ax-7 1441  ax-gen 1442  ax-ie1 1486  ax-ie2 1487  ax-8 1497  ax-11 1499  ax-4 1503  ax-17 1519  ax-i9 1523  ax-ial 1527  ax-i5r 1528  ax-ext 2152

This theorem depends on definitions:  df-bi 116  df-nf 1454  df-sb 1756  df-clab 2157  df-cleq 2163  df-clel 2166  df-in 3127  df-ss 3134

This theorem is referenced by:  cossxp2  5134  fimacnv  5625  smores2  6273  f1imaen2g  6771  phplem4dom  6840  isinfinf  6875  fidcenumlemrk  6931  casef  7065  genipv  7471  fzossnn0  10131  seq3split  10435  1arith  12319  ctinf  12385  nninfdclemcl  12403  nninfdclemp1  12405  mhmima  12706  tgcl  12858  epttop  12884  ntrin  12918  cnconst2  13027  cnrest2  13030  cnptopresti  13032  cnptoprest2  13034  hmeores  13109  blin2  13226  ivthdec  13416  limcdifap  13425  limcresi  13429  dvfgg  13451  dvcnp2cntop  13457  dvaddxxbr  13459  reeff1olem  13486