Theorem syl5req 2183

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 2182	. 2 |- ( ph -> A = C )
4	3	eqcomd 2143	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 2119

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

This theorem is referenced by:  syl5reqr  2185  opeqsn  4169  dcextest  4490  relop  4684  funopg  5152  funcnvres  5191  mapsnconst  6581  snexxph  6831  apreap  8342  recextlem1  8405  nn0supp  9022  intqfrac2  10085  hashprg  10547  hashfacen  10572  explecnv  11267  rerestcntop  12708