Theorem syl5req 2186

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

Hypotheses

Ref	Expression
syl5req.1	⊢ 𝐴 = 𝐵
syl5req.2	⊢ (𝜑 → 𝐵 = 𝐶)

Assertion

Ref	Expression
syl5req	⊢ (𝜑 → 𝐶 = 𝐴)

Proof of Theorem syl5req

Step	Hyp	Ref	Expression
1		syl5req.1	. . 3 ⊢ 𝐴 = 𝐵
2		syl5req.2	. . 3 ⊢ (𝜑 → 𝐵 = 𝐶)
3	1, 2	syl5eq 2185	. 2 ⊢ (𝜑 → 𝐴 = 𝐶)
4	3	eqcomd 2146	1 ⊢ (𝜑 → 𝐶 = 𝐴)

Syntax hints:   → wi 4   = wceq 1332

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 1424  ax-gen 1426  ax-4 1488  ax-17 1507  ax-ext 2122

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

This theorem is referenced by:  syl5reqr  2188  opeqsn  4182  dcextest  4503  relop  4697  funopg  5165  funcnvres  5204  mapsnconst  6596  snexxph  6846  apreap  8373  recextlem1  8436  nn0supp  9053  intqfrac2  10123  hashprg  10586  hashfacen  10611  explecnv  11306  rerestcntop  12758