Theorem syl5eqss 3412

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

Syntax hints:   -> wi 4   = wceq 1369   C_ wss 3340

This theorem was proved from axioms:  ax-mp 5  ax-1 6  ax-2 7  ax-3 8  ax-gen 1591  ax-4 1602  ax-5 1670  ax-6 1708  ax-7 1728  ax-10 1775  ax-11 1780  ax-12 1792  ax-13 1943  ax-ext 2423

This theorem depends on definitions:  df-bi 185  df-an 371  df-tru 1372  df-ex 1587  df-nf 1590  df-sb 1701  df-clab 2430  df-cleq 2436  df-clel 2439  df-in 3347  df-ss 3354

This theorem is referenced by:  syl5eqssr  3413  inss  3591  tpssi  4051  xpsspw  4965  xpsspwOLD  4966  fun  5587  fmpt  5876  fliftrel  6013  knatar  6060  opabbrex  6142  suppss2OLD  6327  fr3nr  6403  suceloni  6436  opabex2  6528  fun11iun  6549  1stcof  6616  2ndcof  6617  fnwelem  6699  oeeui  7053  cantnfp1lem1OLD  7924  cantnfp1lem3OLD  7926  cantnflem1dOLD  7931  cantnflem1OLD  7932  aceq3lem  8302  cflecard  8434  cfslb2n  8449  itunitc1  8601  axdc3lem2  8632  fpwwe2lem12  8820  canthwelem  8829  wuncval2  8926  gruiun  8978  peano5nni  10337  un0addcl  10625  un0mulcl  10626  mertenslem2  13357  4sqlem11  14028  4sqlem19  14036  vdwlem13  14066  imasless  14490  rescfth  14859  oppchofcl  15082  oyoncl  15092  gsumvallem1  15512  efgsfo  16248  efgcpbllemb  16264  frgpuplem  16281  gsumzaddlemOLD  16422  gsummpt1n0  16468  dprdfid  16519  dprdfidOLD  16526  dprd2d2  16555  ablfacrp  16579  ablfac1b  16583  ablfac1eu  16586  pgpfac1lem5  16592  ablfaclem3  16600  lsptpcl  17072  lsppratlem3  17242  lsppratlem4  17243  lbsextlem2  17252  f1lindf  18263  topsn  18552  ordtbaslem  18804  ordtuni  18806  ordtbas2  18807  cnpco  18883  cnconst2  18899  tgcmp  19016  iuncon  19044  ptuni2  19161  xkococnlem  19244  tgqtop  19297  fbasrn  19469  uzrest  19482  fmco  19546  alexsubALT  19635  cnextf  19650  snclseqg  19698  ustund  19808  imasdsf1olem  19960  xmetresbl  20024  blsscls2  20091  metustssOLD  20140  metustss  20141  tngtopn  20248  reconn  20417  metnrmlem3  20449  cphsubrglem  20708  minveclem1  20923  minveclem3b  20927  ovolficcss  20965  ovolicc2lem4  21015  iundisj2  21042  uniioombllem4  21078  vitalilem5  21104  mbfeqalem  21132  itg1addlem4  21189  limciun  21381  dvlip2  21479  dv11cn  21485  aalioulem3  21812  pserdvlem2  21905  pserdv  21906  abelthlem2  21909  efif1o  22014  efrlim  22375  fsumdvdsmul  22547  perfectlem2  22581  usgrares1  23335  eupares  23608  minvecolem1  24287  sh0le  24855  mdslmd3i  25748  iundisj2f  25944  suppss2f  25966  suppss3  26039  iundisj2fi  26093  pstmfval  26335  eulerpartlemt  26766  eulerpartlemmf  26770  eulerpartlemgf  26774  lgamgulmlem1  27027  blscon  27145  cvmliftlem2  27187  cvmlift2lem12  27215  ghomfo  27322  relexpdm  27349  relexprn  27350  trpredss  27705  trpredmintr  27707  frrlem5d  27787  mblfinlem3  28442  areacirclem2  28497  neibastop2lem  28593  filnetlem3  28613  sdclem1  28651  istotbnd3  28682  sstotbnd  28686  iccbnd  28751  icccmpALT  28752  hbtlem6  29497  iocinico  29599  stoweidlem14  29821  fsuppmapnn0fiublem  30810  fsuppmapnn0fiub  30811  dmatsgrp  30890  scmatsgrp  30897  iunconlem2  31683  bnj849  31930  bnj1136  32000  bnj1311  32027  bnj1413  32038  bnj1452  32055  osumcllem1N  33612  osumcllem2N  33613  osumcllem4N  33615  osumcllem9N  33620  pexmidlem6N  33631  dihglblem3N  34952  dvhdimlem  35101  dochexmidlem6  35122  lcfrlem16  35215  lcfr  35242