Theorem syl5eqss 3649

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

Syntax hints:   -> wi 4   = wceq 1483   C_ wss 3574

This theorem was proved from axioms:  ax-mp 5  ax-1 6  ax-2 7  ax-3 8  ax-gen 1722  ax-4 1737  ax-5 1839  ax-6 1888  ax-7 1935  ax-9 1999  ax-10 2019  ax-11 2034  ax-12 2047  ax-13 2246  ax-ext 2602

This theorem depends on definitions:  df-bi 197  df-or 385  df-an 386  df-tru 1486  df-ex 1705  df-nf 1710  df-sb 1881  df-clab 2609  df-cleq 2615  df-clel 2618  df-in 3581  df-ss 3588

This theorem is referenced by:  syl5eqssr  3650  inss  3842  tpssi  4369  xpsspw  5233  opabssxpd  5338  fun  6066  fmpt  6381  fliftrel  6558  knatar  6607  fr3nr  6979  suceloni  7013  fun11iun  7126  1stcof  7196  2ndcof  7197  fnwelem  7292  oeeui  7682  aceq3lem  8943  cflecard  9075  cfslb2n  9090  itunitc1  9242  axdc3lem2  9273  fpwwe2lem12  9463  canthwelem  9472  wuncval2  9569  peano5nni  11023  un0addcl  11326  un0mulcl  11327  fsuppmapnn0fiublem  12789  fsuppmapnn0fiub  12790  fsuppmapnn0fiubOLD  12791  mertenslem2  14617  4sqlem11  15659  4sqlem19  15667  vdwlem13  15697  imasless  16200  rescfth  16597  oppchofcl  16900  oyoncl  16910  mgmidsssn0  17269  efgsfo  18152  efgcpbllemb  18168  frgpuplem  18185  gsummpt1n0  18364  dprdfid  18416  dprd2d2  18443  ablfacrp  18465  ablfac1b  18469  ablfac1eu  18472  pgpfac1lem5  18478  ablfaclem3  18486  lsptpcl  18979  lsppratlem3  19149  lsppratlem4  19150  lbsextlem2  19159  f1lindf  20161  topsn  20735  ordtbaslem  20992  ordtuni  20994  ordtbas2  20995  cnpco  21071  cnconst2  21087  tgcmp  21204  iunconn  21231  ptuni2  21379  xkococnlem  21462  tgqtop  21515  fbasrn  21688  uzrest  21701  fmco  21765  alexsubALT  21855  cnextf  21870  snclseqg  21919  ustund  22025  imasdsf1olem  22178  xmetresbl  22242  blsscls2  22309  metustss  22356  tngtopn  22454  reconn  22631  metnrmlem3  22664  cphsubrglem  22977  minveclem1  23195  minveclem3b  23199  ovolficcss  23238  ovolicc2lem4  23288  iundisj2  23317  uniioombllem4  23354  vitalilem5  23381  mbfeqalem  23409  itg1addlem4  23466  limciun  23658  dvlip2  23758  dv11cn  23764  aalioulem3  24089  pserdvlem2  24182  pserdv  24183  abelthlem2  24186  efif1o  24292  efrlim  24696  lgamgulmlem1  24755  fsumdvdsmul  24921  perfectlem2  24955  setsvtx  25927  uhgredgn0  26023  upgredgss  26027  umgredgss  26028  usgredgss  26054  umgrres1lem  26202  upgrres1  26205  1hegrvtxdg1r  26404  minvecolem1  27730  sh0le  28299  mdslmd3i  29191  iundisj2f  29403  suppss2f  29439  suppss3  29502  iundisj2fi  29556  pstmfval  29939  ordtrest2NEW  29969  ldgenpisyslem1  30226  ldgenpisyslem2  30227  omsmeas  30385  sitgclbn  30405  eulerpartlemt  30433  eulerpartlemmf  30437  eulerpartlemgf  30441  bnj849  30995  bnj1136  31065  bnj1311  31092  bnj1413  31103  bnj1452  31120  blsconn  31226  cvmliftlem2  31268  cvmlift2lem12  31296  mvtss  31450  mthmpps  31479  trpredss  31729  trpredmintr  31731  frrlem5d  31787  noextendseq  31820  nosupno  31849  nosupbnd2lem1  31861  noetalem3  31865  neibastop2lem  32355  filnetlem3  32375  finxpsuclem  33234  poimirlem3  33412  mblfinlem3  33448  areacirclem2  33501  sdclem1  33539  istotbnd3  33570  sstotbnd  33574  iccbnd  33639  icccmpALT  33640  osumcllem1N  35242  osumcllem2N  35243  osumcllem4N  35245  osumcllem9N  35250  pexmidlem6N  35261  dihglblem3N  36584  dvhdimlem  36733  dochexmidlem6  36754  lcfrlem16  36847  lcfr  36874  hbtlem6  37699  iocinico  37797  trclubgNEW  37925  cnvrcl0  37932  relexp0a  38008  brtrclfv2  38019  cotrclrcl  38034  frege77d  38038  unhe1  38079  ntrrn  38420  imo72b2lem0  38465  imo72b2lem2  38467  imo72b2lem1  38471  imo72b2  38475  radcnvrat  38513  iunconnlem2  39171  ssinss2d  39228  limccog  39852  limsupresico  39932  liminfresico  40003  icccncfext  40100  stoweidlem14  40231  fourierdlem20  40344  fourierdlem42  40366  fourierdlem46  40369  fourierdlem50  40373  fourierdlem51  40374  fourierdlem54  40377  fourierdlem64  40387  fourierdlem76  40399  fourierdlem102  40425  fourierdlem103  40426  fourierdlem104  40427  fourierdlem114  40437  meadjiunlem  40682  meaiininclem  40700  ovnsupge0  40771  hoidmvlelem2  40810  hoidmvlelem4  40812  vonvolmbllem  40874  vonvolmbl2  40877  vonvol2  40878  vonioolem1  40894  issmflem  40936  perfectALTVlem2  41631  uspgropssxp  41752  funcrngcsetc  41998  funcringcsetc  42035  srhmsubc  42076  rhmsubclem3  42088  srhmsubcALTV  42094  rhmsubcALTVlem4  42107  setrec2fun  42439  onsetreclem2  42449