Theorem syl5eqss 3352

Description: B chained subclass and equality deduction. (Contributed by NM, 25-Apr-2004.)

Hypotheses

Ref	Expression
syl5eqss.1	|- A = B
syl5eqss.2	|- ( ph -> B C_ C )

Assertion

Ref	Expression
syl5eqss	|- ( ph -> A C_ C )

Proof of Theorem syl5eqss

Step	Hyp	Ref	Expression
1		syl5eqss.2	. 2 |- ( ph -> B C_ C )
2		syl5eqss.1	. . 3 |- A = B
3	2	sseq1i 3332	. 2 |- ( A C_ C <-> B C_ C )
4	1, 3	sylibr 204	1 |- ( ph -> A C_ C )

Syntax hints:   -> wi 4   = wceq 1649   C_ wss 3280

This theorem is referenced by:  syl5eqssr  3353  inss  3530  tpssi  3925  fr3nr  4719  suceloni  4752  xpsspw  4945  xpsspwOLD  4946  fun  5566  fun11iun  5654  fmpt  5849  fliftrel  5989  knatar  6039  opabbrex  6077  suppss2  6259  1stcof  6333  2ndcof  6334  fnwelem  6420  oeeui  6804  cantnfp1lem1  7590  cantnfp1lem3  7592  cantnflem1d  7600  cantnflem1  7601  aceq3lem  7957  cflecard  8089  cfslb2n  8104  itunitc1  8256  axdc3lem2  8287  fpwwe2lem12  8472  canthwelem  8481  wuncval2  8578  gruiun  8630  peano5nni  9959  un0addcl  10209  un0mulcl  10210  mertenslem2  12617  4sqlem11  13278  4sqlem19  13286  vdwlem13  13316  imasless  13720  rescfth  14089  oppchofcl  14312  oyoncl  14322  gsumvallem1  14726  efgsfo  15326  efgcpbllemb  15342  frgpuplem  15359  gsumzaddlem  15481  dprdfid  15530  dprd2d2  15557  ablfacrp  15579  ablfac1b  15583  ablfac1eu  15586  pgpfac1lem5  15592  ablfaclem3  15600  lsptpcl  16010  lsppratlem3  16176  lsppratlem4  16177  lbsextlem2  16186  topsn  16955  ordtbaslem  17206  ordtuni  17208  ordtbas2  17209  cnpco  17285  cnconst2  17301  tgcmp  17418  iuncon  17444  ptuni2  17561  xkococnlem  17644  tgqtop  17697  fbasrn  17869  uzrest  17882  fmco  17946  alexsubALT  18035  cnextf  18050  snclseqg  18098  ustund  18204  imasdsf1olem  18356  xmetresbl  18420  blsscls2  18487  metustssOLD  18536  metustss  18537  tngtopn  18644  reconn  18812  metnrmlem3  18844  cphsubrglem  19093  minveclem1  19278  minveclem3b  19282  ovolficcss  19319  ovolicc2lem4  19369  iundisj2  19396  uniioombllem4  19431  vitalilem5  19457  mbfeqalem  19487  itg1addlem4  19544  limciun  19734  dvlip2  19832  dv11cn  19838  aalioulem3  20204  pserdvlem2  20297  pserdv  20298  abelthlem2  20301  efif1o  20401  efrlim  20761  fsumdvdsmul  20933  perfectlem2  20967  usgrares1  21377  eupares  21650  minvecolem1  22329  sh0le  22895  mdslmd3i  23788  iundisj2f  23983  suppss2f  24002  iundisj2fi  24106  pstmfval  24244  lgamgulmlem1  24766  blscon  24884  cvmliftlem2  24926  cvmlift2lem12  24954  ghomfo  25055  relexpdm  25088  relexprn  25089  trpredss  25446  trpredmintr  25448  frrlem5d  25502  mblfinlem2  26144  areacirclem4  26183  neibastop2lem  26279  filnetlem3  26299  sdclem1  26337  istotbnd3  26370  sstotbnd  26374  iccbnd  26439  icccmpALT  26440  f1lindf  27160  hbtlem6  27201  stoweidlem14  27630  bnj849  29002  bnj1136  29072  bnj1311  29099  bnj1413  29110  bnj1452  29127  osumcllem1N  30438  osumcllem2N  30439  osumcllem4N  30441  osumcllem9N  30446  pexmidlem6N  30457  dihglblem3N  31778  dvhdimlem  31927  dochexmidlem6  31948  lcfrlem16  32041  lcfr  32068

This theorem was proved from axioms:  ax-1 5  ax-2 6  ax-3 7  ax-mp 8  ax-gen 1552  ax-5 1563  ax-17 1623  ax-9 1662  ax-8 1683  ax-6 1740  ax-7 1745  ax-11 1757  ax-12 1946  ax-ext 2385

This theorem depends on definitions:  df-bi 178  df-an 361  df-tru 1325  df-ex 1548  df-nf 1551  df-sb 1656  df-clab 2391  df-cleq 2397  df-clel 2400  df-in 3287  df-ss 3294