Theorem eqtr2id 2203

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

Hypotheses

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

Assertion

Ref	Expression
eqtr2id	⊢ (𝜑 → 𝐶 = 𝐴)

Proof of Theorem eqtr2id

Step	Hyp	Ref	Expression
1		eqtr2id.1	. . 3 ⊢ 𝐴 = 𝐵
2		eqtr2id.2	. . 3 ⊢ (𝜑 → 𝐵 = 𝐶)
3	1, 2	syl5eq 2202	. 2 ⊢ (𝜑 → 𝐴 = 𝐶)
4	3	eqcomd 2163	1 ⊢ (𝜑 → 𝐶 = 𝐴)

Syntax hints:   → wi 4   = wceq 1335

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 1427  ax-gen 1429  ax-4 1490  ax-17 1506  ax-ext 2139

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

This theorem is referenced by:  eqtr3di  2205  opeqsn  4215  dcextest  4543  relop  4739  funopg  5207  funcnvres  5246  mapsnconst  6642  snexxph  6897  apreap  8467  recextlem1  8530  nn0supp  9148  intqfrac2  10228  hashprg  10694  hashfacen  10719  explecnv  11414  rerestcntop  13046  binom4  13393