Theorem eqsstrid 3229

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 3209	. 2 |- ( A C_ C <-> B C_ C )
4	1, 3	sylibr 134	1 |- ( ph -> A C_ C )

Syntax hints:   -> wi 4   = wceq 1364   C_ wss 3157

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 1461  ax-7 1462  ax-gen 1463  ax-ie1 1507  ax-ie2 1508  ax-8 1518  ax-11 1520  ax-4 1524  ax-17 1540  ax-i9 1544  ax-ial 1548  ax-i5r 1549  ax-ext 2178

This theorem depends on definitions:  df-bi 117  df-nf 1475  df-sb 1777  df-clab 2183  df-cleq 2189  df-clel 2192  df-in 3163  df-ss 3170

This theorem is referenced by:  eqsstrrid  3230  inss  3393  difsnss  3768  tpssi  3789  peano5  4634  xpsspw  4775  iotanul  5234  iotass  5236  fun  5430  fun11iun  5525  fvss  5572  fmpt  5712  fliftrel  5839  opabbrex  5966  1stcof  6221  2ndcof  6222  tfrlemibacc  6384  tfrlemibfn  6386  tfr1onlemssrecs  6397  tfr1onlembacc  6400  tfr1onlembfn  6402  tfrcllemssrecs  6410  tfrcllembacc  6413  tfrcllembfn  6415  caucvgprlemladdrl  7745  peano5nnnn  7959  peano5nni  8993  un0addcl  9282  un0mulcl  9283  4sqlemafi  12564  4sqlemffi  12565  4sqleminfi  12566  4sqlem11  12570  4sqlem19  12578  strleund  12781  mgmidsssn0  13027  lsptpcl  13950  cnptopco  14458  cnconst2  14469  xmetresbl  14676  blsscls2  14729  perfectlem2  15236  bj-omtrans  15602