Theorem syl6req 2525

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

Syntax hints:   -> wi 4   = wceq 1379

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-ext 2445

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

This theorem is referenced by:  syl6reqr  2527  csbin  3860  csbif  3989  csbuni  4273  csbima12  5354  somincom  5404  csbfv12  5901  opabiotafun  5928  fndifnfp  6090  elxp4  6728  elxp5  6729  fo1stres  6808  fo2ndres  6809  eloprabi  6846  fo2ndf  6890  seqomlem2  7116  oev2  7173  odi  7228  fundmen  7589  xpsnen  7601  xpassen  7611  ac6sfi  7764  infeq5  8054  alephsuc3  8955  rankcf  9155  ine0  9992  nn0n0n1ge2  10859  fzval2  11675  fseq1p1m1  11752  hashfun  12461  hashf1  12472  hashtpg  12489  cshword  12725  fsum2dlem  13548  ef4p  13709  sin01bnd  13781  odd2np1  13905  bitsinvp1  13958  smumullem  14001  oppcmon  14994  issubc2  15066  curf1cl  15355  curfcl  15359  cnvtsr  15709  sylow1lem1  16424  sylow2a  16445  coe1fzgsumdlem  18142  evl1gsumdlem  18191  pmatcollpw3lem  19079  pptbas  19303  2ndcctbss  19750  txcmplem1  19905  qtopeu  19980  alexsubALTlem3  20312  ustuqtop5  20511  psmetdmdm  20572  xmetdmdm  20601  pcopt  21285  pcorevlem  21289  voliunlem1  21723  i1fima2  21849  iblabs  21998  dveflem  22143  deg1val  22259  deg1valOLD  22260  abssinper  22672  mulcxplem  22821  dvatan  23022  lgseisenlem1  23380  dchrisumlem1  23430  pntlemr  23543  krippenlem  23803  usgra2wlkspthlem1  24323  wlknwwlknsur  24416  grporndm  24916  ismgm  25026  ismndo2  25051  vafval  25200  smfval  25202  hvmul0  25645  cmcmlem  26213  cmbr3i  26222  nmbdfnlbi  26672  nmcfnlbi  26675  nmopcoadji  26724  pjin2i  26816  hst1h  26850  xaddeq0  27269  archirngz  27423  esumcst  27739  omsfval  27933  dstfrvunirn  28081  sgnmul  28149  lgamgulmlem2  28240  lgamgulmlem5  28243  subfacp1lem5  28296  cvmliftlem10  28407  ghomfo  28534  fprod2dlem  28715  ovoliunnfl  29661  voliunnfl  29663  volsupnfl  29664  itg2addnclem  29671  itg2addnc  29674  iblabsnc  29684  iblmulc2nc  29685  fnessref  29793  fnemeet2  29816  sdclem2  29866  blbnd  29914  mzpcompact2lem  30316  diophrw  30324  eldioph2  30327  pellexlem5  30401  pell1qr1  30439  rmxy0  30491  uhgrepe  31873  usgfis  31941  usgfisALT  31945  tendo0co2  35602  dvhfvadd  35906  dvh4dimN  36262