Theorem eqtr2id 2284

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

This proof depends on syntax axioms:   → wi 4   = wceq 1402

This proof depends on axioms:  ax-mp 5  ax-1 6  ax-2 7  ax-ia1 106  ax-ia2 107  ax-ia3 108  ax-5 1500  ax-gen 1502  ax-4 1563  ax-17 1579  ax-ext 2220

This proof depends on definitions:  df-bi 117  df-cleq 2231

This theorem is used by:  eqtr3di  2286  opeqsn  4395  dcextest  4730  relop  4932  funopg  5414  funcnvres  5457  mapsnconst  6982  snexxph  7274  apreap  8923  recextlem1  8987  nn0supp  9628  intqfrac2  10776  hashprg  11270  hashfacen  11305  ccatrid  11396  explecnv  12296  grp1inv  13970  rnrhmsubrg  14668  rerestcntop  15801  rerest  15803  mpomulcn  15809  binom4  16236  wlkvtxedg  16826  wlkres  16842