Theorem eqtr2id 2217

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

Syntax hints:   → wi 4   = wceq 1349

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 1441  ax-gen 1443  ax-4 1504  ax-17 1520  ax-ext 2153

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

This theorem is referenced by:  eqtr3di  2219  opeqsn  4238  dcextest  4566  relop  4762  funopg  5234  funcnvres  5273  mapsnconst  6676  snexxph  6931  apreap  8510  recextlem1  8573  nn0supp  9191  intqfrac2  10279  hashprg  10747  hashfacen  10775  explecnv  11472  grp1inv  12810  rerestcntop  13429  binom4  13776