Theorem eqsstrid 3239

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

Syntax hints:   -> wi 4   = wceq 1373   C_ wss 3166

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 1470  ax-7 1471  ax-gen 1472  ax-ie1 1516  ax-ie2 1517  ax-8 1527  ax-11 1529  ax-4 1533  ax-17 1549  ax-i9 1553  ax-ial 1557  ax-i5r 1558  ax-ext 2187

This theorem depends on definitions:  df-bi 117  df-nf 1484  df-sb 1786  df-clab 2192  df-cleq 2198  df-clel 2201  df-in 3172  df-ss 3179

This theorem is referenced by:  eqsstrrid  3240  inss  3403  difsnss  3779  tpssi  3800  peano5  4647  xpsspw  4788  iotanul  5248  iotass  5250  fun  5450  fun11iun  5545  fvss  5592  fmpt  5732  fliftrel  5863  ovssunirng  5981  opabbrex  5991  1stcof  6251  2ndcof  6252  tfrlemibacc  6414  tfrlemibfn  6416  tfr1onlemssrecs  6427  tfr1onlembacc  6430  tfr1onlembfn  6432  tfrcllemssrecs  6440  tfrcllembacc  6443  tfrcllembfn  6445  caucvgprlemladdrl  7793  peano5nnnn  8007  peano5nni  9041  un0addcl  9330  un0mulcl  9331  4sqlemafi  12751  4sqlemffi  12752  4sqleminfi  12753  4sqlem11  12757  4sqlem19  12765  strleund  12968  mgmidsssn0  13249  lsptpcl  14189  cnptopco  14727  cnconst2  14738  xmetresbl  14945  blsscls2  14998  perfectlem2  15505  bj-omtrans  15929