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  6862  snexxph  7148  apreap  8766  recextlem1  8830  nn0supp  9453  intqfrac2  10580  hashprg  11071  hashfacen  11099  ccatrid  11183  explecnv  12065  grp1inv  13689  rnrhmsubrg  14265  rerestcntop  15281  rerest  15283  mpomulcn  15289  binom4  15702  wlkvtxedg  16213  wlkres  16229