Theorem syl5eqss 3462

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

Syntax hints:   -> wi 4   = wceq 1452   C_ wss 3390

This theorem was proved from axioms:  ax-mp 5  ax-1 6  ax-2 7  ax-3 8  ax-gen 1677  ax-4 1690  ax-5 1766  ax-6 1813  ax-7 1859  ax-10 1932  ax-11 1937  ax-12 1950  ax-13 2104  ax-ext 2451

This theorem depends on definitions:  df-bi 190  df-an 378  df-tru 1455  df-ex 1672  df-nf 1676  df-sb 1806  df-clab 2458  df-cleq 2464  df-clel 2467  df-in 3397  df-ss 3404

This theorem is referenced by:  syl5eqssr  3463  inss  3652  tpssi  4130  xpsspw  4953  fun  5758  fmpt  6058  fliftrel  6219  knatar  6266  fr3nr  6625  suceloni  6659  opabex2  6750  fun11iun  6772  1stcof  6840  2ndcof  6841  fnwelem  6930  oeeui  7321  aceq3lem  8569  cflecard  8701  cfslb2n  8716  itunitc1  8868  axdc3lem2  8899  fpwwe2lem12  9084  canthwelem  9093  wuncval2  9190  peano5nni  10634  un0addcl  10927  un0mulcl  10928  fsuppmapnn0fiublem  12240  fsuppmapnn0fiub  12241  mertenslem2  14018  4sqlem11  14978  4sqlem19  14992  vdwlem13  15022  imasless  15524  rescfth  15920  oppchofcl  16223  oyoncl  16233  mgmidsssn0  16590  efgsfo  17467  efgcpbllemb  17483  frgpuplem  17500  gsummpt1n0  17675  dprdfid  17728  dprd2d2  17755  ablfacrp  17777  ablfac1b  17781  ablfac1eu  17784  pgpfac1lem5  17790  ablfaclem3  17798  lsptpcl  18280  lsppratlem3  18450  lsppratlem4  18451  lbsextlem2  18460  f1lindf  19457  topsn  20027  ordtbaslem  20281  ordtuni  20283  ordtbas2  20284  cnpco  20360  cnconst2  20376  tgcmp  20493  iuncon  20520  ptuni2  20668  xkococnlem  20751  tgqtop  20804  fbasrn  20977  uzrest  20990  fmco  21054  alexsubALT  21144  cnextf  21159  snclseqg  21208  ustund  21314  imasdsf1olem  21466  xmetresbl  21530  blsscls2  21597  metustss  21644  tngtopn  21736  reconn  21924  metnrmlem3  21956  metnrmlem3OLD  21971  cphsubrglem  22233  minveclem1  22444  minveclem3b  22448  minveclem3bOLD  22460  ovolficcss  22500  ovolicc2lem4OLD  22551  ovolicc2lem4  22552  iundisj2  22581  uniioombllem4  22623  vitalilem5  22649  mbfeqalem  22677  itg1addlem4  22736  limciun  22928  dvlip2  23026  dv11cn  23032  aalioulem3  23369  pserdvlem2  23462  pserdv  23463  abelthlem2  23466  efif1o  23574  efrlim  23974  lgamgulmlem1  24033  fsumdvdsmul  24203  perfectlem2  24237  usgrares1  25217  eupares  25782  minvecolem1  26597  sh0le  27174  mdslmd3i  28066  iundisj2f  28277  suppss2fOLD  28313  suppss2f  28314  suppss3  28387  iundisj2fi  28448  pstmfval  28773  ordtrest2NEW  28803  ldgenpisyslem1  29059  ldgenpisyslem2  29060  omsmeas  29228  omsmeasOLD  29229  sitgclbn  29249  eulerpartlemt  29277  eulerpartlemmf  29281  eulerpartlemgf  29285  bnj849  29808  bnj1136  29878  bnj1311  29905  bnj1413  29916  bnj1452  29933  blscon  30039  cvmliftlem2  30081  cvmlift2lem12  30109  mvtss  30263  mthmpps  30292  ghomfo  30381  trpredss  30541  trpredmintr  30543  frrlem5d  30592  neibastop2lem  31087  filnetlem3  31107  finxpsuclem  31859  poimirlem3  32007  mblfinlem3  32043  areacirclem2  32097  sdclem1  32136  istotbnd3  32167  sstotbnd  32171  iccbnd  32236  icccmpALT  32237  osumcllem1N  33592  osumcllem2N  33593  osumcllem4N  33595  osumcllem9N  33600  pexmidlem6N  33611  dihglblem3N  34934  dvhdimlem  35083  dochexmidlem6  35104  lcfrlem16  35197  lcfr  35224  hbtlem6  36059  iocinico  36167  trclubgNEW  36296  cnvrcl0  36303  relexp0a  36379  brtrclfv2  36390  cotrclrcl  36405  frege77d  36409  unhe1  36452  imo72b2lem0  36679  imo72b2lem2  36681  imo72b2lem1  36685  imo72b2  36689  radcnvrat  36733  iunconlem2  37395  ssinss2d  37459  limccog  37797  icccncfext  37862  stoweidlem14  37986  fourierdlem20  38101  fourierdlem42  38124  fourierdlem42OLD  38125  fourierdlem46  38128  fourierdlem50  38132  fourierdlem51  38133  fourierdlem54  38136  fourierdlem64  38146  fourierdlem76  38158  fourierdlem102  38184  fourierdlem103  38185  fourierdlem104  38186  fourierdlem114  38196  meadjiunlem  38419  ovnsupge0  38497  hoidmvlelem2  38536  hoidmvlelem4  38538  vonvolmbllem  38600  vonvolmbl2  38603  vonvol2  38604  perfectALTVlem2  38989  umgrres1lem  39541  upgrres1  39544  1hegrvtxdg1r  39731  usgresvm1  40263  usgresvm1ALT  40267  funcrngcsetc  40508  funcringcsetc  40545  srhmsubc  40586  rhmsubclem3  40598  srhmsubcALTV  40605  rhmsubcALTVlem4  40618