Theorem eqsstrid 3226

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 3206	. 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 3154

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 1458  ax-7 1459  ax-gen 1460  ax-ie1 1504  ax-ie2 1505  ax-8 1515  ax-11 1517  ax-4 1521  ax-17 1537  ax-i9 1541  ax-ial 1545  ax-i5r 1546  ax-ext 2175

This theorem depends on definitions:  df-bi 117  df-nf 1472  df-sb 1774  df-clab 2180  df-cleq 2186  df-clel 2189  df-in 3160  df-ss 3167

This theorem is referenced by:  eqsstrrid  3227  inss  3390  difsnss  3765  tpssi  3786  peano5  4631  xpsspw  4772  iotanul  5231  iotass  5233  fun  5427  fun11iun  5522  fvss  5569  fmpt  5709  fliftrel  5836  opabbrex  5963  1stcof  6218  2ndcof  6219  tfrlemibacc  6381  tfrlemibfn  6383  tfr1onlemssrecs  6394  tfr1onlembacc  6397  tfr1onlembfn  6399  tfrcllemssrecs  6407  tfrcllembacc  6410  tfrcllembfn  6412  caucvgprlemladdrl  7740  peano5nnnn  7954  peano5nni  8987  un0addcl  9276  un0mulcl  9277  4sqlemafi  12536  4sqlemffi  12537  4sqleminfi  12538  4sqlem11  12542  4sqlem19  12550  strleund  12724  mgmidsssn0  12970  lsptpcl  13893  cnptopco  14401  cnconst2  14412  xmetresbl  14619  blsscls2  14672  bj-omtrans  15518