Theorem eqtr2id 2277

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	eqtrid 2276	. 2 ⊢ (𝜑 → 𝐴 = 𝐶)
4	3	eqcomd 2237	1 ⊢ (𝜑 → 𝐶 = 𝐴)

Syntax hints:   → wi 4   = wceq 1397

This theorem was proved from axioms:  ax-mp 5  ax-1 6  ax-2 7  ax-ia1 106  ax-ia2 107  ax-ia3 108  ax-5 1495  ax-gen 1497  ax-4 1558  ax-17 1574  ax-ext 2213

This theorem depends on definitions:  df-bi 117  df-cleq 2224

This theorem is referenced by:  eqtr3di  2279  opeqsn  4345  dcextest  4679  relop  4880  funopg  5360  funcnvres  5403  mapsnconst  6863  snexxph  7149  apreap  8767  recextlem1  8831  nn0supp  9454  intqfrac2  10582  hashprg  11073  hashfacen  11101  ccatrid  11188  explecnv  12084  grp1inv  13708  rnrhmsubrg  14285  rerestcntop  15301  rerest  15303  mpomulcn  15309  binom4  15722  wlkvtxedg  16233  wlkres  16249