Theorem eqtr2id 2278

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

Syntax hints:   → wi 4   = wceq 1398

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 1496  ax-gen 1498  ax-4 1559  ax-17 1575  ax-ext 2214

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

This theorem is referenced by:  eqtr3di  2280  opeqsn  4369  dcextest  4703  relop  4905  funopg  5386  funcnvres  5429  mapsnconst  6929  snexxph  7220  apreap  8861  recextlem1  8925  nn0supp  9552  intqfrac2  10681  hashprg  11173  hashfacen  11208  ccatrid  11295  explecnv  12191  grp1inv  13820  rnrhmsubrg  14397  rerestcntop  15423  rerest  15425  mpomulcn  15431  binom4  15844  wlkvtxedg  16358  wlkres  16374