Theorem sstrid 3181

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

Syntax hints:   -> wi 4   C_ wss 3144

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 1458  ax-7 1459  ax-gen 1460  ax-ie1 1504  ax-ie2 1505  ax-8 1515  ax-11 1517  ax-4 1521  ax-17 1537  ax-i9 1541  ax-ial 1545  ax-i5r 1546  ax-ext 2171

This theorem depends on definitions:  df-bi 117  df-nf 1472  df-sb 1774  df-clab 2176  df-cleq 2182  df-clel 2185  df-in 3150  df-ss 3157

This theorem is referenced by:  cossxp2  5170  fimacnv  5666  smores2  6320  f1imaen2g  6820  phplem4dom  6891  isinfinf  6926  fidcenumlemrk  6984  casef  7118  genipv  7539  fzossnn0  10207  seq3split  10512  1arith  12402  ctinf  12484  nninfdclemcl  12502  nninfdclemp1  12504  mhmima  12958  tgcl  14041  epttop  14067  ntrin  14101  cnconst2  14210  cnrest2  14213  cnptopresti  14215  cnptoprest2  14217  hmeores  14292  blin2  14409  ivthdec  14599  limcdifap  14608  limcresi  14612  dvfgg  14634  dvcnp2cntop  14640  dvaddxxbr  14642  reeff1olem  14669