Theorem syl6req 2453

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

Syntax hints:   -> wi 4   = wceq 1649

This theorem is referenced by:  syl6reqr  2455  somincom  5230  elxp4  5316  elxp5  5317  fo1stres  6329  fo2ndres  6330  eloprabi  6372  fo2ndf  6412  opabiotafun  6495  seqomlem2  6667  oev2  6726  odi  6781  fundmen  7139  xpsnen  7151  xpassen  7161  ac6sfi  7310  infeq5  7548  alephsuc3  8411  rankcf  8608  ine0  9425  nn0n0n1ge2  10236  fzval2  11002  fseq1p1m1  11077  hashtpg  11646  hashfun  11655  hashf1  11661  fsum2dlem  12509  ef4p  12669  sin01bnd  12741  odd2np1  12863  bitsinvp1  12916  smumullem  12959  oppcmon  13919  issubc2  13991  curf1cl  14280  curfcl  14284  cnvtsr  14609  sylow1lem1  15187  sylow2a  15208  pptbas  17027  2ndcctbss  17471  txcmplem1  17626  qtopeu  17701  alexsubALTlem3  18033  ustuqtop5  18228  psmetdmdm  18289  xmetdmdm  18318  pcopt  19000  pcorevlem  19004  voliunlem1  19397  i1fima2  19524  iblabs  19673  dveflem  19816  deg1val  19972  abssinper  20379  mulcxplem  20528  dvatan  20728  lgseisenlem1  21086  dchrisumlem1  21136  pntlemr  21249  grporndm  21751  ismgm  21861  ismndo2  21886  vafval  22035  smfval  22037  hvmul0  22479  cmcmlem  23046  cmbr3i  23055  nmbdfnlbi  23505  nmcfnlbi  23508  nmopcoadji  23557  pjin2i  23649  hst1h  23683  xaddeq0  24072  esumcst  24408  dstfrvunirn  24685  lgamgulmlem2  24767  lgamgulmlem5  24770  subfacp1lem5  24823  cvmliftlem10  24934  ghomfo  25055  fprod2dlem  25257  ovoliunnfl  26147  voliunnfl  26149  volsupnfl  26150  itg2addnclem  26155  itg2addnc  26158  iblabsnc  26168  iblmulc2nc  26169  fnessref  26263  fnemeet2  26286  sdclem2  26336  blbnd  26386  fndifnfp  26627  mzpcompact2lem  26698  diophrw  26707  eldioph2  26710  pellexlem5  26786  pell1qr1  26824  rmxy0  26876  usgra2wlkspthlem1  28036  tendo0co2  31270  dvhfvadd  31574  dvh4dimN  31930

This theorem was proved from axioms:  ax-1 5  ax-2 6  ax-3 7  ax-mp 8  ax-gen 1552  ax-5 1563  ax-17 1623  ax-9 1662  ax-8 1683  ax-11 1757  ax-ext 2385

This theorem depends on definitions:  df-bi 178  df-ex 1548  df-cleq 2397