Theorem syl5eqss 3508

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

Syntax hints:   -> wi 4   = wceq 1437   C_ wss 3436

This theorem was proved from axioms:  ax-mp 5  ax-1 6  ax-2 7  ax-3 8  ax-gen 1665  ax-4 1678  ax-5 1748  ax-6 1794  ax-7 1839  ax-10 1887  ax-11 1892  ax-12 1905  ax-13 2053  ax-ext 2400

This theorem depends on definitions:  df-bi 188  df-an 372  df-tru 1440  df-ex 1660  df-nf 1664  df-sb 1787  df-clab 2408  df-cleq 2414  df-clel 2417  df-in 3443  df-ss 3450

This theorem is referenced by:  syl5eqssr  3509  inss  3691  tpssi  4163  xpsspw  4963  fun  5759  fmpt  6054  fliftrel  6212  knatar  6259  opabbrexOLD  6344  fr3nr  6616  suceloni  6650  opabex2  6741  fun11iun  6763  1stcof  6831  2ndcof  6832  fnwelem  6918  oeeui  7307  aceq3lem  8551  cflecard  8683  cfslb2n  8698  itunitc1  8850  axdc3lem2  8881  fpwwe2lem12  9066  canthwelem  9075  wuncval2  9172  peano5nni  10612  un0addcl  10903  un0mulcl  10904  fsuppmapnn0fiublem  12201  fsuppmapnn0fiub  12202  mertenslem2  13928  4sqlem11  14886  4sqlem19  14900  vdwlem13  14930  imasless  15433  rescfth  15829  oppchofcl  16132  oyoncl  16142  mgmidsssn0  16499  efgsfo  17376  efgcpbllemb  17392  frgpuplem  17409  gsummpt1n0  17584  dprdfid  17637  dprd2d2  17664  ablfacrp  17686  ablfac1b  17690  ablfac1eu  17693  pgpfac1lem5  17699  ablfaclem3  17707  lsptpcl  18189  lsppratlem3  18359  lsppratlem4  18360  lbsextlem2  18369  f1lindf  19366  topsn  19936  ordtbaslem  20190  ordtuni  20192  ordtbas2  20193  cnpco  20269  cnconst2  20285  tgcmp  20402  iuncon  20429  ptuni2  20577  xkococnlem  20660  tgqtop  20713  fbasrn  20885  uzrest  20898  fmco  20962  alexsubALT  21052  cnextf  21067  snclseqg  21116  ustund  21222  imasdsf1olem  21374  xmetresbl  21438  blsscls2  21505  metustss  21552  tngtopn  21644  reconn  21832  metnrmlem3  21864  metnrmlem3OLD  21879  cphsubrglem  22141  minveclem1  22352  minveclem3b  22356  minveclem3bOLD  22368  ovolficcss  22408  ovolicc2lem4OLD  22459  ovolicc2lem4  22460  iundisj2  22488  uniioombllem4  22530  vitalilem5  22556  mbfeqalem  22584  itg1addlem4  22643  limciun  22835  dvlip2  22933  dv11cn  22939  aalioulem3  23276  pserdvlem2  23369  pserdv  23370  abelthlem2  23373  efif1o  23481  efrlim  23881  lgamgulmlem1  23940  fsumdvdsmul  24110  perfectlem2  24144  usgrares1  25123  eupares  25688  minvecolem1  26501  sh0le  27078  mdslmd3i  27970  iundisj2f  28189  suppss2fOLD  28226  suppss2f  28227  suppss3  28305  iundisj2fi  28366  pstmfval  28694  ordtrest2NEW  28724  ldgenpisyslem1  28980  ldgenpisyslem2  28981  omsmeas  29150  omsmeasOLD  29151  sitgclbn  29171  eulerpartlemt  29199  eulerpartlemmf  29203  eulerpartlemgf  29207  bnj849  29731  bnj1136  29801  bnj1311  29828  bnj1413  29839  bnj1452  29856  blscon  29962  cvmliftlem2  30004  cvmlift2lem12  30032  mvtss  30186  mthmpps  30215  ghomfo  30304  trpredss  30464  trpredmintr  30466  frrlem5d  30515  neibastop2lem  31008  filnetlem3  31028  poimirlem3  31856  mblfinlem3  31892  areacirclem2  31946  sdclem1  31985  istotbnd3  32016  sstotbnd  32020  iccbnd  32085  icccmpALT  32086  osumcllem1N  33439  osumcllem2N  33440  osumcllem4N  33442  osumcllem9N  33447  pexmidlem6N  33458  dihglblem3N  34781  dvhdimlem  34930  dochexmidlem6  34951  lcfrlem16  35044  lcfr  35071  hbtlem6  35907  iocinico  36015  relexp0a  36167  brtrclfv2  36178  cotrclrcl  36193  frege77d  36197  unhe1  36238  imo72b2lem0  36465  imo72b2lem2  36467  imo72b2lem1  36471  imo72b2  36476  radcnvrat  36520  iunconlem2  37192  ssinss2d  37261  limccog  37519  icccncfext  37584  stoweidlem14  37693  fourierdlem20  37808  fourierdlem42  37831  fourierdlem42OLD  37832  fourierdlem46  37835  fourierdlem50  37839  fourierdlem51  37840  fourierdlem54  37843  fourierdlem64  37853  fourierdlem76  37865  fourierdlem102  37891  fourierdlem103  37892  fourierdlem104  37893  fourierdlem114  37903  meadjiunlem  38081  ovnsupge0  38153  perfectALTVlem2  38555  usgresvm1  39026  usgresvm1ALT  39030  funcrngcsetc  39271  funcringcsetc  39308  srhmsubc  39349  rhmsubclem3  39361  srhmsubcALTV  39368  rhmsubcALTVlem4  39381