Theorem eqsstrid 3247

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 3227	. 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 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:  eqsstrrid  3248  inss  3411  difsnss  3790  tpssi  3813  peano5  4664  xpsspw  4805  iotanul  5266  iotass  5268  fun  5469  fun11iun  5565  fvss  5613  fmpt  5753  fliftrel  5884  ovssunirng  6002  opabbrex  6012  1stcof  6272  2ndcof  6273  tfrlemibacc  6435  tfrlemibfn  6437  tfr1onlemssrecs  6448  tfr1onlembacc  6451  tfr1onlembfn  6453  tfrcllemssrecs  6461  tfrcllembacc  6464  tfrcllembfn  6466  caucvgprlemladdrl  7826  peano5nnnn  8040  peano5nni  9074  un0addcl  9363  un0mulcl  9364  4sqlemafi  12833  4sqlemffi  12834  4sqleminfi  12835  4sqlem11  12839  4sqlem19  12847  strleund  13050  mgmidsssn0  13331  lsptpcl  14271  cnptopco  14809  cnconst2  14820  xmetresbl  15027  blsscls2  15080  perfectlem2  15587  bj-omtrans  16091