Theorem syl6req 2513

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 2512	. 2 |- ( ph -> A = C )
4	3	eqcomd 2468	1 |- ( ph -> C = A )

Syntax hints:   -> wi 4   = wceq 1455

This theorem was proved from axioms:  ax-mp 5  ax-1 6  ax-2 7  ax-3 8  ax-gen 1680  ax-4 1693  ax-ext 2442

This theorem depends on definitions:  df-bi 190  df-cleq 2455

This theorem is referenced by:  syl6reqr  2515  csbin  3811  csbif  3943  csbuni  4240  csbima12  5204  somincom  5253  csbfv12  5923  opabiotafun  5949  fndifnfp  6117  elxp4  6764  elxp5  6765  fo1stres  6844  fo2ndres  6845  eloprabi  6882  fo2ndf  6930  seqomlem2  7194  oev2  7251  odi  7306  fundmen  7669  xpsnen  7682  xpassen  7692  ac6sfi  7841  infeq5  8168  alephsuc3  9031  rankcf  9228  ine0  10082  nn0n0n1ge2  10961  fzval2  11816  fseq1p1m1  11897  hashfun  12642  hashf1  12653  hashtpg  12674  cshword  12930  wrd2pr2op  13068  wrd3tpop  13072  fsum2dlem  13880  fprod2dlem  14083  ef4p  14216  sin01bnd  14288  odd2np1  14414  bitsinvp1  14472  smumullem  14515  oppcmon  15692  issubc2  15790  curf1cl  16162  curfcl  16166  cnvtsr  16517  sylow1lem1  17299  sylow2a  17320  coe1fzgsumdlem  18944  evl1gsumdlem  18993  pmatcollpw3lem  19856  pptbas  20072  2ndcctbss  20519  txcmplem1  20705  qtopeu  20780  alexsubALTlem3  21113  ustuqtop5  21309  psmetdmdm  21370  xmetdmdm  21399  pcopt  22102  pcorevlem  22106  voliunlem1  22552  i1fima2  22686  iblabs  22835  dveflem  22980  deg1val  23094  abssinper  23522  mulcxplem  23678  dvatan  23910  lgamgulmlem2  24004  lgamgulmlem5  24007  lgseisenlem1  24326  dchrisumlem1  24376  pntlemr  24489  krippenlem  24784  usgra2wlkspthlem1  25396  wlknwwlknsur  25489  grporndm  25987  ismgmOLD  26097  ismndo2  26122  vafval  26271  smfval  26273  hvmul0  26726  cmcmlem  27293  cmbr3i  27302  nmbdfnlbi  27751  nmcfnlbi  27754  nmopcoadji  27803  pjin2i  27895  hst1h  27929  xaddeq0  28379  archirngz  28555  esumcst  28933  eulerpartlems  29242  dstfrvunirn  29356  sgnmul  29462  subfacp1lem5  29956  cvmliftlem10  30066  ghomfo  30358  fnessref  31062  fnemeet2  31072  poimirlem4  31989  poimirlem19  32004  poimirlem20  32005  poimirlem23  32008  poimirlem24  32009  poimirlem25  32010  poimirlem28  32013  ovoliunnfl  32027  voliunnfl  32029  volsupnfl  32030  itg2addnclem  32038  itg2addnc  32041  iblabsnc  32051  iblmulc2nc  32052  sdclem2  32116  blbnd  32164  tendo0co2  34400  dvhfvadd  34704  dvh4dimN  35060  mzpcompact2lem  35638  diophrw  35646  eldioph2  35649  pellexlem5  35722  pell1qr1  35762  rmxy0  35816  cncfuni  37802  cncfiooicclem1  37809  fourierdlem38  38046  fourierdlem60  38068  fourierdlem61  38069  fourierdlem79  38087  fourierdlem112  38120  fourierswlem  38132  fouriersw  38133  cshword2  39018  resresdm  39050  cusgredg  39542  cusgrsizeindb0  39560  uhgrepe  39963  usgfis  40031  usgfisALT  40035  nn0sumshdiglem1  40705