Theorem syl5eqss 3548

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

Syntax hints:   -> wi 4   = wceq 1379   C_ wss 3476

This theorem was proved from axioms:  ax-mp 5  ax-1 6  ax-2 7  ax-3 8  ax-gen 1601  ax-4 1612  ax-5 1680  ax-6 1719  ax-7 1739  ax-10 1786  ax-11 1791  ax-12 1803  ax-13 1968  ax-ext 2445

This theorem depends on definitions:  df-bi 185  df-an 371  df-tru 1382  df-ex 1597  df-nf 1600  df-sb 1712  df-clab 2453  df-cleq 2459  df-clel 2462  df-in 3483  df-ss 3490

This theorem is referenced by:  syl5eqssr  3549  inss  3727  tpssi  4193  xpsspw  5114  xpsspwOLD  5115  fun  5746  fmpt  6040  fliftrel  6192  knatar  6239  opabbrex  6322  suppss2OLD  6512  fr3nr  6593  suceloni  6626  opabex2  6719  fun11iun  6741  1stcof  6809  2ndcof  6810  fnwelem  6895  oeeui  7248  cantnfp1lem1OLD  8119  cantnfp1lem3OLD  8121  cantnflem1dOLD  8126  cantnflem1OLD  8127  aceq3lem  8497  cflecard  8629  cfslb2n  8644  itunitc1  8796  axdc3lem2  8827  fpwwe2lem12  9015  canthwelem  9024  wuncval2  9121  gruiun  9173  peano5nni  10535  un0addcl  10825  un0mulcl  10826  fsuppmapnn0fiublem  12059  fsuppmapnn0fiub  12060  mertenslem2  13650  4sqlem11  14325  4sqlem19  14333  vdwlem13  14363  imasless  14788  rescfth  15157  oppchofcl  15380  oyoncl  15390  gsumvallem1  15810  efgsfo  16550  efgcpbllemb  16566  frgpuplem  16583  gsumzaddlemOLD  16724  gsummpt1n0  16780  dprdfid  16844  dprdfidOLD  16851  dprd2d2  16880  ablfacrp  16904  ablfac1b  16908  ablfac1eu  16911  pgpfac1lem5  16917  ablfaclem3  16925  lsptpcl  17405  lsppratlem3  17575  lsppratlem4  17576  lbsextlem2  17585  f1lindf  18621  topsn  19200  ordtbaslem  19452  ordtuni  19454  ordtbas2  19455  cnpco  19531  cnconst2  19547  tgcmp  19664  iuncon  19692  ptuni2  19809  xkococnlem  19892  tgqtop  19945  fbasrn  20117  uzrest  20130  fmco  20194  alexsubALT  20283  cnextf  20298  snclseqg  20346  ustund  20456  imasdsf1olem  20608  xmetresbl  20672  blsscls2  20739  metustssOLD  20788  metustss  20789  tngtopn  20896  reconn  21065  metnrmlem3  21097  cphsubrglem  21356  minveclem1  21571  minveclem3b  21575  ovolficcss  21613  ovolicc2lem4  21663  iundisj2  21691  uniioombllem4  21727  vitalilem5  21753  mbfeqalem  21781  itg1addlem4  21838  limciun  22030  dvlip2  22128  dv11cn  22134  aalioulem3  22461  pserdvlem2  22554  pserdv  22555  abelthlem2  22558  efif1o  22663  efrlim  23024  fsumdvdsmul  23196  perfectlem2  23230  usgrares1  24083  eupares  24648  minvecolem1  25463  sh0le  26031  mdslmd3i  26924  iundisj2f  27119  suppss2f  27147  suppss3  27219  iundisj2fi  27267  pstmfval  27508  eulerpartlemt  27947  eulerpartlemmf  27951  eulerpartlemgf  27955  lgamgulmlem1  28208  blscon  28326  cvmliftlem2  28368  cvmlift2lem12  28396  ghomfo  28503  relexpdm  28530  relexprn  28531  trpredss  28886  trpredmintr  28888  frrlem5d  28968  mblfinlem3  29628  areacirclem2  29683  neibastop2lem  29779  filnetlem3  29799  sdclem1  29837  istotbnd3  29868  sstotbnd  29872  iccbnd  29937  icccmpALT  29938  hbtlem6  30682  iocinico  30784  icccncfext  31226  stoweidlem14  31314  fourierdlem20  31427  fourierdlem42  31449  fourierdlem46  31453  fourierdlem50  31457  fourierdlem51  31458  fourierdlem54  31461  fourierdlem64  31471  fourierdlem76  31483  fourierdlem102  31509  fourierdlem103  31510  fourierdlem104  31511  fourierdlem114  31521  usgresvm1  31912  usgresvm1ALT  31916  iunconlem2  32815  bnj849  33062  bnj1136  33132  bnj1311  33159  bnj1413  33170  bnj1452  33187  osumcllem1N  34752  osumcllem2N  34753  osumcllem4N  34755  osumcllem9N  34760  pexmidlem6N  34771  dihglblem3N  36092  dvhdimlem  36241  dochexmidlem6  36262  lcfrlem16  36355  lcfr  36382