Theorem syl5eqss 3397

Description: A 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 3377	. 2 |- ( A C_ C <-> B C_ C )
4	1, 3	sylibr 212	1 |- ( ph -> A C_ C )

Syntax hints:   -> wi 4   = wceq 1364   C_ wss 3325

This theorem was proved from axioms:  ax-mp 5  ax-1 6  ax-2 7  ax-3 8  ax-gen 1596  ax-4 1607  ax-5 1675  ax-6 1713  ax-7 1733  ax-10 1780  ax-11 1785  ax-12 1797  ax-13 1948  ax-ext 2422

This theorem depends on definitions:  df-bi 185  df-an 371  df-ex 1592  df-nf 1595  df-sb 1706  df-clab 2428  df-cleq 2434  df-clel 2437  df-in 3332  df-ss 3339

This theorem is referenced by:  syl5eqssr  3398  inss  3576  tpssi  4036  xpsspw  4949  xpsspwOLD  4950  fun  5572  fmpt  5861  fliftrel  5998  knatar  6045  opabbrex  6129  suppss2OLD  6314  fr3nr  6390  suceloni  6423  opabex2  6515  fun11iun  6536  1stcof  6603  2ndcof  6604  fnwelem  6686  oeeui  7037  cantnfp1lem1OLD  7908  cantnfp1lem3OLD  7910  cantnflem1dOLD  7915  cantnflem1OLD  7916  aceq3lem  8286  cflecard  8418  cfslb2n  8433  itunitc1  8585  axdc3lem2  8616  fpwwe2lem12  8804  canthwelem  8813  wuncval2  8910  gruiun  8962  peano5nni  10321  un0addcl  10609  un0mulcl  10610  mertenslem2  13341  4sqlem11  14012  4sqlem19  14020  vdwlem13  14050  imasless  14474  rescfth  14843  oppchofcl  15066  oyoncl  15076  gsumvallem1  15495  efgsfo  16229  efgcpbllemb  16245  frgpuplem  16262  gsumzaddlemOLD  16403  gsummptif1n0  16447  dprdfid  16497  dprdfidOLD  16504  dprd2d2  16533  ablfacrp  16557  ablfac1b  16561  ablfac1eu  16564  pgpfac1lem5  16570  ablfaclem3  16578  lsptpcl  17038  lsppratlem3  17208  lsppratlem4  17209  lbsextlem2  17218  f1lindf  18210  topsn  18499  ordtbaslem  18751  ordtuni  18753  ordtbas2  18754  cnpco  18830  cnconst2  18846  tgcmp  18963  iuncon  18991  ptuni2  19108  xkococnlem  19191  tgqtop  19244  fbasrn  19416  uzrest  19429  fmco  19493  alexsubALT  19582  cnextf  19597  snclseqg  19645  ustund  19755  imasdsf1olem  19907  xmetresbl  19971  blsscls2  20038  metustssOLD  20087  metustss  20088  tngtopn  20195  reconn  20364  metnrmlem3  20396  cphsubrglem  20655  minveclem1  20870  minveclem3b  20874  ovolficcss  20912  ovolicc2lem4  20962  iundisj2  20989  uniioombllem4  21025  vitalilem5  21051  mbfeqalem  21079  itg1addlem4  21136  limciun  21328  dvlip2  21426  dv11cn  21432  aalioulem3  21759  pserdvlem2  21852  pserdv  21853  abelthlem2  21856  efif1o  21961  efrlim  22322  fsumdvdsmul  22494  perfectlem2  22528  usgrares1  23258  eupares  23531  minvecolem1  24210  sh0le  24778  mdslmd3i  25671  iundisj2f  25867  suppss2f  25889  suppss3  25962  iundisj2fi  26014  pstmfval  26259  eulerpartlemt  26684  eulerpartlemmf  26688  eulerpartlemgf  26692  lgamgulmlem1  26945  blscon  27063  cvmliftlem2  27105  cvmlift2lem12  27133  ghomfo  27239  relexpdm  27266  relexprn  27267  trpredss  27622  trpredmintr  27624  frrlem5d  27704  mblfinlem3  28355  areacirclem2  28410  neibastop2lem  28506  filnetlem3  28526  sdclem1  28564  istotbnd3  28595  sstotbnd  28599  iccbnd  28664  icccmpALT  28665  hbtlem6  29410  iocinico  29512  stoweidlem14  29734  dmatsgrp  30761  scmatsgrp  30768  iunconlem2  31505  bnj849  31752  bnj1136  31822  bnj1311  31849  bnj1413  31860  bnj1452  31877  osumcllem1N  33322  osumcllem2N  33323  osumcllem4N  33325  osumcllem9N  33330  pexmidlem6N  33341  dihglblem3N  34662  dvhdimlem  34811  dochexmidlem6  34832  lcfrlem16  34925  lcfr  34952