Theorem eqsstrid 3284

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 3264	. 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 3211

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 2214

This theorem depends on definitions:  df-bi 117  df-nf 1510  df-sb 1812  df-clab 2219  df-cleq 2225  df-clel 2228  df-in 3217  df-ss 3224

This theorem is referenced by:  eqsstrrid  3285  inss  3451  difsnss  3840  tpssi  3863  peano5  4720  opabssxpd  4786  xpsspw  4862  iotanul  5328  iotass  5330  fun  5536  fun11iun  5635  fvss  5684  fmpt  5827  fliftrel  5965  ovssunirng  6085  opabbrex  6097  1stcof  6357  2ndcof  6358  tfrlemibacc  6557  tfrlemibfn  6559  tfr1onlemssrecs  6570  tfr1onlembacc  6573  tfr1onlembfn  6575  tfrcllemssrecs  6583  tfrcllembacc  6586  tfrcllembfn  6588  caucvgprlemladdrl  7993  peano5nnnn  8207  peano5nni  9240  un0addcl  9529  un0mulcl  9530  4sqlemafi  13093  4sqlemffi  13094  4sqleminfi  13095  4sqlem11  13099  4sqlem19  13107  strleund  13316  mgmidsssn0  13597  lsptpcl  14542  cnptopco  15087  cnconst2  15098  xmetresbl  15305  blsscls2  15358  perfectlem2  15868  setsvtx  16046  1hegrvtxdg1rfi  16305  bj-omtrans  16726