Theorem syl6req 2512

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

Syntax hints:   -> wi 4   = wceq 1398

This theorem was proved from axioms:  ax-mp 5  ax-1 6  ax-2 7  ax-3 8  ax-gen 1623  ax-4 1636  ax-ext 2432

This theorem depends on definitions:  df-bi 185  df-cleq 2446

This theorem is referenced by:  syl6reqr  2514  csbin  3849  csbif  3979  csbuni  4263  csbima12  5342  somincom  5389  csbfv12  5883  opabiotafun  5909  fndifnfp  6076  elxp4  6717  elxp5  6718  fo1stres  6797  fo2ndres  6798  eloprabi  6835  fo2ndf  6880  seqomlem2  7108  oev2  7165  odi  7220  fundmen  7582  xpsnen  7594  xpassen  7604  ac6sfi  7756  infeq5  8045  alephsuc3  8946  rankcf  9144  ine0  9988  nn0n0n1ge2  10855  fzval2  11678  fseq1p1m1  11756  hashfun  12479  hashf1  12490  hashtpg  12507  cshword  12753  fsum2dlem  13667  fprod2dlem  13866  ef4p  13930  sin01bnd  14002  odd2np1  14130  bitsinvp1  14183  smumullem  14226  oppcmon  15226  issubc2  15324  curf1cl  15696  curfcl  15700  cnvtsr  16051  sylow1lem1  16817  sylow2a  16838  coe1fzgsumdlem  18538  evl1gsumdlem  18587  pmatcollpw3lem  19451  pptbas  19676  2ndcctbss  20122  txcmplem1  20308  qtopeu  20383  alexsubALTlem3  20715  ustuqtop5  20914  psmetdmdm  20975  xmetdmdm  21004  pcopt  21688  pcorevlem  21692  voliunlem1  22126  i1fima2  22252  iblabs  22401  dveflem  22546  deg1val  22662  deg1valOLD  22663  abssinper  23077  mulcxplem  23233  dvatan  23463  lgseisenlem1  23822  dchrisumlem1  23872  pntlemr  23985  krippenlem  24268  usgra2wlkspthlem1  24821  wlknwwlknsur  24914  grporndm  25410  ismgmOLD  25520  ismndo2  25545  vafval  25694  smfval  25696  hvmul0  26139  cmcmlem  26707  cmbr3i  26716  nmbdfnlbi  27166  nmcfnlbi  27169  nmopcoadji  27218  pjin2i  27310  hst1h  27344  xaddeq0  27804  archirngz  27967  esumcst  28292  eulerpartlems  28563  dstfrvunirn  28677  sgnmul  28745  lgamgulmlem2  28836  lgamgulmlem5  28839  subfacp1lem5  28892  cvmliftlem10  29003  ghomfo  29295  ovoliunnfl  30296  voliunnfl  30298  volsupnfl  30299  itg2addnclem  30306  itg2addnc  30309  iblabsnc  30319  iblmulc2nc  30320  fnessref  30415  fnemeet2  30425  sdclem2  30475  blbnd  30523  mzpcompact2lem  30923  diophrw  30931  eldioph2  30934  pellexlem5  31008  pell1qr1  31046  rmxy0  31098  cncfuni  31928  cncfiooicclem1  31935  fourierdlem38  32166  fourierdlem60  32188  fourierdlem61  32189  fourierdlem79  32207  fourierdlem112  32240  fourierswlem  32252  fouriersw  32253  cshword2  32665  uhgrepe  32750  usgfis  32818  usgfisALT  32822  nn0sumshdiglem1  33496  tendo0co2  36911  dvhfvadd  37215  dvh4dimN  37571