Theorem sstrid 3212

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

Syntax hints:   -> wi 4   C_ wss 3174

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 1471  ax-7 1472  ax-gen 1473  ax-ie1 1517  ax-ie2 1518  ax-8 1528  ax-11 1530  ax-4 1534  ax-17 1550  ax-i9 1554  ax-ial 1558  ax-i5r 1559  ax-ext 2189

This theorem depends on definitions:  df-bi 117  df-nf 1485  df-sb 1787  df-clab 2194  df-cleq 2200  df-clel 2203  df-in 3180  df-ss 3187

This theorem is referenced by:  cossxp2  5225  fimacnv  5732  smores2  6403  f1imaen2g  6908  phplem4dom  6984  isinfinf  7020  fidcenumlemrk  7082  casef  7216  genipv  7657  fzossnn0  10334  seq3split  10670  1arith  12805  ctinf  12916  nninfdclemcl  12934  nninfdclemp1  12936  mhmima  13438  znleval  14530  tgcl  14651  epttop  14677  ntrin  14711  cnconst2  14820  cnrest2  14823  cnptopresti  14825  cnptoprest2  14827  hmeores  14902  blin2  15019  ivthdec  15231  limcdifap  15249  limcresi  15253  dvfgg  15275  dvcnp2cntop  15286  dvaddxxbr  15288  reeff1olem  15358  domomsubct  16140