Theorem eqtr2id 2280

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

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

This theorem is referenced by:  eqtr3di  2282  opeqsn  4374  dcextest  4708  relop  4910  funopg  5391  funcnvres  5434  mapsnconst  6942  snexxph  7233  apreap  8878  recextlem1  8942  nn0supp  9569  intqfrac2  10705  hashprg  11198  hashfacen  11233  ccatrid  11320  explecnv  12216  grp1inv  13862  rnrhmsubrg  14498  rerestcntop  15549  rerest  15551  mpomulcn  15557  binom4  15970  wlkvtxedg  16484  wlkres  16500