Theorem syl5eqss 3543

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

Syntax hints:   -> wi 4   = wceq 1395   C_ wss 3471

This theorem was proved from axioms:  ax-mp 5  ax-1 6  ax-2 7  ax-3 8  ax-gen 1619  ax-4 1632  ax-5 1705  ax-6 1748  ax-7 1791  ax-10 1838  ax-11 1843  ax-12 1855  ax-13 2000  ax-ext 2435

This theorem depends on definitions:  df-bi 185  df-an 371  df-tru 1398  df-ex 1614  df-nf 1618  df-sb 1741  df-clab 2443  df-cleq 2449  df-clel 2452  df-in 3478  df-ss 3485

This theorem is referenced by:  syl5eqssr  3544  inss  3723  tpssi  4198  xpsspw  5125  xpsspwOLD  5126  fun  5754  fmpt  6053  fliftrel  6207  knatar  6254  opabbrexOLD  6339  suppss2OLD  6529  fr3nr  6614  suceloni  6647  opabex2  6737  fun11iun  6759  1stcof  6827  2ndcof  6828  fnwelem  6914  oeeui  7269  cantnfp1lem1OLD  8140  cantnfp1lem3OLD  8142  cantnflem1dOLD  8147  cantnflem1OLD  8148  aceq3lem  8518  cflecard  8650  cfslb2n  8665  itunitc1  8817  axdc3lem2  8848  fpwwe2lem12  9036  canthwelem  9045  wuncval2  9142  peano5nni  10559  un0addcl  10850  un0mulcl  10851  fsuppmapnn0fiublem  12098  fsuppmapnn0fiub  12099  mertenslem2  13705  4sqlem11  14484  4sqlem19  14492  vdwlem13  14522  imasless  14956  rescfth  15352  oppchofcl  15655  oyoncl  15665  mgmidsssn0  16022  efgsfo  16883  efgcpbllemb  16899  frgpuplem  16916  gsumzaddlemOLD  17062  gsummpt1n0  17118  dprdfid  17183  dprdfidOLD  17190  dprd2d2  17219  ablfacrp  17243  ablfac1b  17247  ablfac1eu  17250  pgpfac1lem5  17256  ablfaclem3  17264  lsptpcl  17751  lsppratlem3  17921  lsppratlem4  17922  lbsextlem2  17931  f1lindf  18983  topsn  19562  ordtbaslem  19815  ordtuni  19817  ordtbas2  19818  cnpco  19894  cnconst2  19910  tgcmp  20027  iuncon  20054  ptuni2  20202  xkococnlem  20285  tgqtop  20338  fbasrn  20510  uzrest  20523  fmco  20587  alexsubALT  20676  cnextf  20691  snclseqg  20739  ustund  20849  imasdsf1olem  21001  xmetresbl  21065  blsscls2  21132  metustssOLD  21181  metustss  21182  tngtopn  21289  reconn  21458  metnrmlem3  21490  cphsubrglem  21749  minveclem1  21964  minveclem3b  21968  ovolficcss  22006  ovolicc2lem4  22056  iundisj2  22084  uniioombllem4  22120  vitalilem5  22146  mbfeqalem  22174  itg1addlem4  22231  limciun  22423  dvlip2  22521  dv11cn  22527  aalioulem3  22855  pserdvlem2  22948  pserdv  22949  abelthlem2  22952  efif1o  23058  efrlim  23424  fsumdvdsmul  23596  perfectlem2  23630  usgrares1  24536  eupares  25101  minvecolem1  25916  sh0le  26484  mdslmd3i  27377  iundisj2f  27586  suppss2f  27620  suppss3  27700  iundisj2fi  27754  pstmfval  28028  ordtrest2NEW  28058  sitgclbn  28460  eulerpartlemt  28485  eulerpartlemmf  28489  eulerpartlemgf  28493  lgamgulmlem1  28746  blscon  28864  cvmliftlem2  28906  cvmlift2lem12  28934  mvtss  29088  mthmpps  29117  ghomfo  29206  relexpdm  29233  relexprn  29234  trpredss  29486  trpredmintr  29488  frrlem5d  29568  mblfinlem3  30215  areacirclem2  30270  neibastop2lem  30340  filnetlem3  30360  sdclem1  30398  istotbnd3  30429  sstotbnd  30433  iccbnd  30498  icccmpALT  30499  hbtlem6  31240  iocinico  31341  radcnvrat  31357  limccog  31787  icccncfext  31851  stoweidlem14  31957  fourierdlem20  32070  fourierdlem42  32092  fourierdlem46  32096  fourierdlem50  32100  fourierdlem51  32101  fourierdlem54  32104  fourierdlem64  32114  fourierdlem76  32126  fourierdlem102  32152  fourierdlem103  32153  fourierdlem104  32154  fourierdlem114  32164  usgresvm1  32663  usgresvm1ALT  32667  funcrngcsetc  32908  funcringcsetc  32945  srhmsubc  32986  rhmsubclem3  32998  srhmsubcOLD  33005  rhmsubcOLDlem4  33018  iunconlem2  33836  bnj849  34084  bnj1136  34154  bnj1311  34181  bnj1413  34192  bnj1452  34209  osumcllem1N  35781  osumcllem2N  35782  osumcllem4N  35784  osumcllem9N  35789  pexmidlem6N  35800  dihglblem3N  37123  dvhdimlem  37272  dochexmidlem6  37293  lcfrlem16  37386  lcfr  37413  unhe1  37909  imo72b2lem0  38083  imo72b2lem2  38085  imo72b2lem1  38089  imo72b2  38094