Theorem eqsstrid 3288

Description: B chained subclass and equality deduction. (Contributed by NM, 25-Apr-2004.)

Hypotheses

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

Assertion

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

Proof of Theorem eqsstrid

Step	Hyp	Ref	Expression
1		eqsstrid.2	. 2 |- ( ph -> B C_ C )
2		eqsstrid.1	. . 3 |- A = B
3	2	sseq1i 3268	. 2 |- ( A C_ C <-> B C_ C )
4	1, 3	sylibr 134	1 |- ( ph -> A C_ C )

Syntax hints:   -> wi 4   = wceq 1398   C_ wss 3214

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 1496  ax-7 1497  ax-gen 1498  ax-ie1 1542  ax-ie2 1543  ax-8 1553  ax-11 1555  ax-4 1559  ax-17 1575  ax-i9 1579  ax-ial 1583  ax-i5r 1584  ax-ext 2216

This theorem depends on definitions:  df-bi 117  df-nf 1510  df-sb 1812  df-clab 2221  df-cleq 2227  df-clel 2230  df-in 3220  df-ss 3227

This theorem is referenced by:  eqsstrrid  3289  inss  3455  difsnss  3845  tpssi  3868  peano5  4725  opabssxpd  4791  xpsspw  4867  iotanul  5333  iotass  5335  fun  5541  fun11iun  5640  fvss  5689  fmpt  5832  fliftrel  5971  ovssunirng  6093  opabbrex  6105  1stcof  6370  2ndcof  6371  tfrlemibacc  6570  tfrlemibfn  6572  tfr1onlemssrecs  6583  tfr1onlembacc  6586  tfr1onlembfn  6588  tfrcllemssrecs  6596  tfrcllembacc  6599  tfrcllembfn  6601  caucvgprlemladdrl  8009  peano5nnnn  8223  peano5nni  9257  un0addcl  9546  un0mulcl  9547  4sqlemafi  13118  4sqlemffi  13119  4sqleminfi  13120  4sqlem11  13124  4sqlem19  13132  strleund  13400  mgmidsssn0  13647  lsptpcl  14668  cnptopco  15213  cnconst2  15224  xmetresbl  15431  blsscls2  15484  perfectlem2  15994  setsvtx  16172  1hegrvtxdg1rfi  16431  bj-omtrans  16852