Theorem syl5req 2185

Description: An equality transitivity deduction. (Contributed by NM, 29-Mar-1998.)

Hypotheses

Ref	Expression
syl5req.1	|- A = B
syl5req.2	|- ( ph -> B = C )

Assertion

Ref	Expression
syl5req	|- ( ph -> C = A )

Proof of Theorem syl5req

Step	Hyp	Ref	Expression
1		syl5req.1	. . 3 |- A = B
2		syl5req.2	. . 3 |- ( ph -> B = C )
3	1, 2	syl5eq 2184	. 2 |- ( ph -> A = C )
4	3	eqcomd 2145	1 |- ( ph -> C = A )

Syntax hints:   -> wi 4   = wceq 1331

This theorem was proved from axioms:  ax-mp 5  ax-1 6  ax-2 7  ax-ia1 105  ax-ia2 106  ax-ia3 107  ax-5 1423  ax-gen 1425  ax-4 1487  ax-17 1506  ax-ext 2121

This theorem depends on definitions:  df-bi 116  df-cleq 2132

This theorem is referenced by:  syl5reqr  2187  opeqsn  4174  dcextest  4495  relop  4689  funopg  5157  funcnvres  5196  mapsnconst  6588  snexxph  6838  apreap  8349  recextlem1  8412  nn0supp  9029  intqfrac2  10092  hashprg  10554  hashfacen  10579  explecnv  11274  rerestcntop  12719