Theorem eqsstrid 3274

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

Syntax hints:   -> wi 4   = wceq 1398   C_ wss 3201

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 1496  ax-7 1497  ax-gen 1498  ax-ie1 1542  ax-ie2 1543  ax-8 1553  ax-11 1555  ax-4 1559  ax-17 1575  ax-i9 1579  ax-ial 1583  ax-i5r 1584  ax-ext 2213

This theorem depends on definitions:  df-bi 117  df-nf 1510  df-sb 1811  df-clab 2218  df-cleq 2224  df-clel 2227  df-in 3207  df-ss 3214

This theorem is referenced by:  eqsstrrid  3275  inss  3439  difsnss  3824  tpssi  3847  peano5  4702  opabssxpd  4768  xpsspw  4844  iotanul  5309  iotass  5311  fun  5516  fun11iun  5613  fvss  5662  fmpt  5805  fliftrel  5943  ovssunirng  6063  opabbrex  6075  1stcof  6335  2ndcof  6336  tfrlemibacc  6535  tfrlemibfn  6537  tfr1onlemssrecs  6548  tfr1onlembacc  6551  tfr1onlembfn  6553  tfrcllemssrecs  6561  tfrcllembacc  6564  tfrcllembfn  6566  caucvgprlemladdrl  7958  peano5nnnn  8172  peano5nni  9205  un0addcl  9494  un0mulcl  9495  4sqlemafi  13048  4sqlemffi  13049  4sqleminfi  13050  4sqlem11  13054  4sqlem19  13062  strleund  13266  mgmidsssn0  13547  lsptpcl  14490  cnptopco  15033  cnconst2  15044  xmetresbl  15251  blsscls2  15304  perfectlem2  15814  setsvtx  15992  1hegrvtxdg1rfi  16251  bj-omtrans  16672