Theorem eqsstrid 3294

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

Syntax hints:   -> wi 4   = wceq 1402   C_ wss 3220

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 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 theorem 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 referenced by:  eqsstrrid  3295  inss  3461  difsnss  3856  tpssi  3879  peano5  4740  opabssxpd  4806  xpsspw  4882  iotanul  5348  iotass  5350  fun  5556  fun11iun  5655  fvss  5704  fmpt  5849  fliftrel  5988  ovssunirng  6110  opabbrex  6122  1stcof  6387  2ndcof  6388  tfrlemibacc  6587  tfrlemibfn  6589  tfr1onlemssrecs  6600  tfr1onlembacc  6603  tfr1onlembfn  6605  tfrcllemssrecs  6613  tfrcllembacc  6616  tfrcllembfn  6618  caucvgprlemladdrl  8035  peano5nnnn  8249  peano5nni  9286  un0addcl  9575  un0mulcl  9576  4sqlemafi  13152  4sqlemffi  13153  4sqleminfi  13154  4sqlem11  13158  4sqlem19  13166  strleund  13434  mgmidsssn0  13681  lsptpcl  14703  cnptopco  15246  cnconst2  15257  xmetresbl  15464  blsscls2  15517  perfectlem2  16028  setsvtx  16206  1hegrvtxdg1rfi  16465  bj-omtrans  16896