Theorem eqsstrid 3203

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

Syntax hints:   -> wi 4   = wceq 1353   C_ wss 3131

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 1447  ax-7 1448  ax-gen 1449  ax-ie1 1493  ax-ie2 1494  ax-8 1504  ax-11 1506  ax-4 1510  ax-17 1526  ax-i9 1530  ax-ial 1534  ax-i5r 1535  ax-ext 2159

This theorem depends on definitions:  df-bi 117  df-nf 1461  df-sb 1763  df-clab 2164  df-cleq 2170  df-clel 2173  df-in 3137  df-ss 3144

This theorem is referenced by:  eqsstrrid  3204  inss  3367  difsnss  3740  tpssi  3761  peano5  4599  xpsspw  4740  iotanul  5195  iotass  5197  fun  5390  fun11iun  5484  fvss  5531  fmpt  5668  fliftrel  5795  opabbrex  5921  1stcof  6166  2ndcof  6167  tfrlemibacc  6329  tfrlemibfn  6331  tfr1onlemssrecs  6342  tfr1onlembacc  6345  tfr1onlembfn  6347  tfrcllemssrecs  6355  tfrcllembacc  6358  tfrcllembfn  6360  caucvgprlemladdrl  7679  peano5nnnn  7893  peano5nni  8924  un0addcl  9211  un0mulcl  9212  strleund  12564  mgmidsssn0  12808  cnptopco  13761  cnconst2  13772  xmetresbl  13979  blsscls2  14032  bj-omtrans  14747