Theorem sstrid 3259

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

This proof depends on syntax axioms:   -> wi 4   C_ wss 3220

This proof depends on axioms:  ax-mp 5  ax-1 6  ax-2 7  ax-ia1 106  ax-ia2 107  ax-ia3 108  ax-5 1500  ax-7 1501  ax-gen 1502  ax-ie1 1546  ax-ie2 1547  ax-8 1557  ax-11 1559  ax-4 1563  ax-17 1579  ax-i9 1583  ax-ial 1587  ax-i5r 1588  ax-ext 2220

This proof depends on definitions:  df-bi 117  df-nf 1514  df-sb 1816  df-clab 2225  df-cleq 2231  df-clel 2234  df-in 3226  df-ss 3233

This theorem is used by:  cossxp2  5311  fimass  5550  fimacnv  5837  smores2  6565  f1imaen2g  7080  phplem4dom  7163  isinfinf  7201  fidcenumlemrk  7271  casef  7428  genipv  7876  fzossnn0  10594  seq3split  10938  1arith  13166  ballotfilemsima  13308  ctinf  13370  nninfdclemcl  13388  nninfdclemp1  13390  mhmima  13847  znleval  15037  tgcl  15214  epttop  15240  ntrin  15274  cnconst2  15383  cnrest2  15386  cnptopresti  15388  cnptoprest2  15390  hmeores  15465  blin2  15582  ivthdec  15794  limcdifap  15812  limcresi  15816  dvfgg  15838  dvcnp2cntop  15849  dvaddxxbr  15851  reeff1olem  15921  ppiqsval  16156  prmdvdsfi  16159  domomsubct  17129