Theorem syl5eqss 3475

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

Syntax hints:   -> wi 4   = wceq 1443   C_ wss 3403

This theorem was proved from axioms:  ax-mp 5  ax-1 6  ax-2 7  ax-3 8  ax-gen 1668  ax-4 1681  ax-5 1757  ax-6 1804  ax-7 1850  ax-10 1914  ax-11 1919  ax-12 1932  ax-13 2090  ax-ext 2430

This theorem depends on definitions:  df-bi 189  df-an 373  df-tru 1446  df-ex 1663  df-nf 1667  df-sb 1797  df-clab 2437  df-cleq 2443  df-clel 2446  df-in 3410  df-ss 3417

This theorem is referenced by:  syl5eqssr  3476  inss  3660  tpssi  4137  xpsspw  4947  fun  5744  fmpt  6041  fliftrel  6199  knatar  6246  opabbrexOLD  6331  fr3nr  6603  suceloni  6637  opabex2  6728  fun11iun  6750  1stcof  6818  2ndcof  6819  fnwelem  6908  oeeui  7300  aceq3lem  8548  cflecard  8680  cfslb2n  8695  itunitc1  8847  axdc3lem2  8878  fpwwe2lem12  9063  canthwelem  9072  wuncval2  9169  peano5nni  10609  un0addcl  10900  un0mulcl  10901  fsuppmapnn0fiublem  12199  fsuppmapnn0fiub  12200  mertenslem2  13934  4sqlem11  14892  4sqlem19  14906  vdwlem13  14936  imasless  15439  rescfth  15835  oppchofcl  16138  oyoncl  16148  mgmidsssn0  16505  efgsfo  17382  efgcpbllemb  17398  frgpuplem  17415  gsummpt1n0  17590  dprdfid  17643  dprd2d2  17670  ablfacrp  17692  ablfac1b  17696  ablfac1eu  17699  pgpfac1lem5  17705  ablfaclem3  17713  lsptpcl  18195  lsppratlem3  18365  lsppratlem4  18366  lbsextlem2  18375  f1lindf  19373  topsn  19943  ordtbaslem  20197  ordtuni  20199  ordtbas2  20200  cnpco  20276  cnconst2  20292  tgcmp  20409  iuncon  20436  ptuni2  20584  xkococnlem  20667  tgqtop  20720  fbasrn  20892  uzrest  20905  fmco  20969  alexsubALT  21059  cnextf  21074  snclseqg  21123  ustund  21229  imasdsf1olem  21381  xmetresbl  21445  blsscls2  21512  metustss  21559  tngtopn  21651  reconn  21839  metnrmlem3  21871  metnrmlem3OLD  21886  cphsubrglem  22148  minveclem1  22359  minveclem3b  22363  minveclem3bOLD  22375  ovolficcss  22415  ovolicc2lem4OLD  22466  ovolicc2lem4  22467  iundisj2  22495  uniioombllem4  22537  vitalilem5  22563  mbfeqalem  22591  itg1addlem4  22650  limciun  22842  dvlip2  22940  dv11cn  22946  aalioulem3  23283  pserdvlem2  23376  pserdv  23377  abelthlem2  23380  efif1o  23488  efrlim  23888  lgamgulmlem1  23947  fsumdvdsmul  24117  perfectlem2  24151  usgrares1  25131  eupares  25696  minvecolem1  26509  sh0le  27086  mdslmd3i  27978  iundisj2f  28193  suppss2fOLD  28230  suppss2f  28231  suppss3  28305  iundisj2fi  28366  pstmfval  28692  ordtrest2NEW  28722  ldgenpisyslem1  28978  ldgenpisyslem2  28979  omsmeas  29148  omsmeasOLD  29149  sitgclbn  29169  eulerpartlemt  29197  eulerpartlemmf  29201  eulerpartlemgf  29205  bnj849  29729  bnj1136  29799  bnj1311  29826  bnj1413  29837  bnj1452  29854  blscon  29960  cvmliftlem2  30002  cvmlift2lem12  30030  mvtss  30184  mthmpps  30213  ghomfo  30302  trpredss  30463  trpredmintr  30465  frrlem5d  30514  neibastop2lem  31009  filnetlem3  31029  finxpsuclem  31782  poimirlem3  31936  mblfinlem3  31972  areacirclem2  32026  sdclem1  32065  istotbnd3  32096  sstotbnd  32100  iccbnd  32165  icccmpALT  32166  osumcllem1N  33515  osumcllem2N  33516  osumcllem4N  33518  osumcllem9N  33523  pexmidlem6N  33534  dihglblem3N  34857  dvhdimlem  35006  dochexmidlem6  35027  lcfrlem16  35120  lcfr  35147  hbtlem6  35982  iocinico  36090  trclubgNEW  36219  cnvrcl0  36226  relexp0a  36302  brtrclfv2  36313  cotrclrcl  36328  frege77d  36332  unhe1  36375  imo72b2lem0  36602  imo72b2lem2  36604  imo72b2lem1  36608  imo72b2  36613  radcnvrat  36657  iunconlem2  37326  ssinss2d  37394  limccog  37694  icccncfext  37759  stoweidlem14  37868  fourierdlem20  37983  fourierdlem42  38006  fourierdlem42OLD  38007  fourierdlem46  38010  fourierdlem50  38014  fourierdlem51  38015  fourierdlem54  38018  fourierdlem64  38028  fourierdlem76  38040  fourierdlem102  38066  fourierdlem103  38067  fourierdlem104  38068  fourierdlem114  38078  meadjiunlem  38297  ovnsupge0  38373  hoidmvlelem2  38412  hoidmvlelem4  38414  perfectALTVlem2  38838  umgrres1lem  39360  upgrres1  39363  usgresvm1  39742  usgresvm1ALT  39746  funcrngcsetc  39987  funcringcsetc  40024  srhmsubc  40065  rhmsubclem3  40077  srhmsubcALTV  40084  rhmsubcALTVlem4  40097