Theorem syl6req 2130

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

Syntax hints:   -> wi 4   = wceq 1284

This theorem was proved from axioms:  ax-1 5  ax-2 6  ax-mp 7  ax-ia1 104  ax-ia2 105  ax-ia3 106  ax-5 1376  ax-gen 1378  ax-4 1440  ax-17 1459  ax-ext 2063

This theorem depends on definitions:  df-bi 115  df-cleq 2074

This theorem is referenced by:  syl6reqr  2132  elxp4  4828  elxp5  4829  fo1stresm  5808  fo2ndresm  5809  eloprabi  5842  fo2ndf  5868  xpsnen  6318  xpassen  6327  ac6sfi  6379  ine0  7498  nn0n0n1ge2  8418  fzval2  9032  fseq1p1m1  9111  odd2np1  10272  sqpweven  10553  2sqpwodd  10554