Theorem syl6req 2482

Description: An equality transitivity deduction. (Contributed by NM, 29-Mar-1998.)

Hypotheses

Ref	Expression
syl6req.1	|- ( ph -> A = B )
syl6req.2	|- B = C

Assertion

Ref	Expression
syl6req	|- ( ph -> C = A )

Proof of Theorem syl6req

Step	Hyp	Ref	Expression
1		syl6req.1	. . 3 |- ( ph -> A = B )
2		syl6req.2	. . 3 |- B = C
3	1, 2	syl6eq 2481	. 2 |- ( ph -> A = C )
4	3	eqcomd 2438	1 |- ( ph -> C = A )

Syntax hints:   -> wi 4   = wceq 1362

This theorem was proved from axioms:  ax-mp 5  ax-1 6  ax-2 7  ax-3 8  ax-gen 1594  ax-4 1605  ax-5 1669  ax-6 1707  ax-7 1727  ax-12 1791  ax-ext 2414

This theorem depends on definitions:  df-bi 185  df-ex 1590  df-cleq 2426

This theorem is referenced by:  syl6reqr  2484  csbin  3700  csbif  3827  csbuni  4107  csbima12  5174  somincom  5223  csbfv12  5713  opabiotafun  5740  fndifnfp  5894  elxp4  6511  elxp5  6512  fo1stres  6589  fo2ndres  6590  eloprabi  6625  fo2ndf  6668  seqomlem2  6892  oev2  6951  odi  7006  fundmen  7371  xpsnen  7383  xpassen  7393  ac6sfi  7544  infeq5  7831  alephsuc3  8732  rankcf  8931  ine0  9767  nn0n0n1ge2  10630  fzval2  11426  fseq1p1m1  11517  hashtpg  12169  hashfun  12182  hashf1  12193  cshword  12411  fsum2dlem  13220  ef4p  13379  sin01bnd  13451  odd2np1  13574  bitsinvp1  13627  smumullem  13670  oppcmon  14659  issubc2  14731  curf1cl  15020  curfcl  15024  cnvtsr  15374  sylow1lem1  16076  sylow2a  16097  pptbas  18453  2ndcctbss  18900  txcmplem1  19055  qtopeu  19130  alexsubALTlem3  19462  ustuqtop5  19661  psmetdmdm  19722  xmetdmdm  19751  pcopt  20435  pcorevlem  20439  voliunlem1  20872  i1fima2  20998  iblabs  21147  dveflem  21292  deg1val  21451  deg1valOLD  21452  abssinper  21864  mulcxplem  22013  dvatan  22214  lgseisenlem1  22572  dchrisumlem1  22622  pntlemr  22735  grporndm  23519  ismgm  23629  ismndo2  23654  vafval  23803  smfval  23805  hvmul0  24248  cmcmlem  24816  cmbr3i  24825  nmbdfnlbi  25275  nmcfnlbi  25278  nmopcoadji  25327  pjin2i  25419  hst1h  25453  xaddeq0  25870  archirngz  26029  esumcst  26367  eulerpartlems  26590  dstfrvunirn  26704  sgnmul  26772  lgamgulmlem2  26863  lgamgulmlem5  26866  subfacp1lem5  26919  cvmliftlem10  27030  ghomfo  27156  fprod2dlem  27337  ovoliunnfl  28274  voliunnfl  28276  volsupnfl  28277  itg2addnclem  28284  itg2addnc  28287  iblabsnc  28297  iblmulc2nc  28298  fnessref  28406  fnemeet2  28429  sdclem2  28479  blbnd  28527  mzpcompact2lem  28930  diophrw  28939  eldioph2  28942  pellexlem5  29016  pell1qr1  29054  rmxy0  29106  usgra2wlkspthlem1  30139  wlknwwlknsur  30187  tendo0co2  34002  dvhfvadd  34306  dvh4dimN  34662