Theorem syl6req 2492

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

Syntax hints:   -> wi 4   = wceq 1369

This theorem was proved from axioms:  ax-mp 5  ax-1 6  ax-2 7  ax-3 8  ax-gen 1591  ax-4 1602  ax-5 1670  ax-6 1708  ax-7 1728  ax-12 1792  ax-ext 2423

This theorem depends on definitions:  df-bi 185  df-ex 1587  df-cleq 2436

This theorem is referenced by:  syl6reqr  2494  csbin  3733  csbif  3860  csbuni  4140  csbima12  5207  somincom  5256  csbfv12  5746  opabiotafun  5773  fndifnfp  5928  elxp4  6543  elxp5  6544  fo1stres  6621  fo2ndres  6622  eloprabi  6657  fo2ndf  6700  seqomlem2  6927  oev2  6984  odi  7039  fundmen  7404  xpsnen  7416  xpassen  7426  ac6sfi  7577  infeq5  7864  alephsuc3  8765  rankcf  8965  ine0  9801  nn0n0n1ge2  10664  fzval2  11461  fseq1p1m1  11555  hashtpg  12207  hashfun  12220  hashf1  12231  cshword  12449  fsum2dlem  13258  ef4p  13418  sin01bnd  13490  odd2np1  13613  bitsinvp1  13666  smumullem  13709  oppcmon  14698  issubc2  14770  curf1cl  15059  curfcl  15063  cnvtsr  15413  sylow1lem1  16118  sylow2a  16139  evl1gsumdlem  17812  pptbas  18634  2ndcctbss  19081  txcmplem1  19236  qtopeu  19311  alexsubALTlem3  19643  ustuqtop5  19842  psmetdmdm  19903  xmetdmdm  19932  pcopt  20616  pcorevlem  20620  voliunlem1  21053  i1fima2  21179  iblabs  21328  dveflem  21473  deg1val  21589  deg1valOLD  21590  abssinper  22002  mulcxplem  22151  dvatan  22352  lgseisenlem1  22710  dchrisumlem1  22760  pntlemr  22873  krippenlem  23106  grporndm  23719  ismgm  23829  ismndo2  23854  vafval  24003  smfval  24005  hvmul0  24448  cmcmlem  25016  cmbr3i  25025  nmbdfnlbi  25475  nmcfnlbi  25478  nmopcoadji  25527  pjin2i  25619  hst1h  25653  xaddeq0  26068  archirngz  26228  esumcst  26536  omsfval  26731  dstfrvunirn  26879  sgnmul  26947  lgamgulmlem2  27038  lgamgulmlem5  27041  subfacp1lem5  27094  cvmliftlem10  27205  ghomfo  27332  fprod2dlem  27513  ovoliunnfl  28459  voliunnfl  28461  volsupnfl  28462  itg2addnclem  28469  itg2addnc  28472  iblabsnc  28482  iblmulc2nc  28483  fnessref  28591  fnemeet2  28614  sdclem2  28664  blbnd  28712  mzpcompact2lem  29114  diophrw  29123  eldioph2  29126  pellexlem5  29200  pell1qr1  29238  rmxy0  29290  usgra2wlkspthlem1  30322  wlknwwlknsur  30370  coe1fzgsumdlem  30870  tendo0co2  34528  dvhfvadd  34832  dvh4dimN  35188