Theorem eqtr2id 2239

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

Syntax hints:   → wi 4   = wceq 1364

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 1458  ax-gen 1460  ax-4 1521  ax-17 1537  ax-ext 2175

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

This theorem is referenced by:  eqtr3di  2241  opeqsn  4281  dcextest  4613  relop  4812  funopg  5288  funcnvres  5327  mapsnconst  6748  snexxph  7009  apreap  8606  recextlem1  8670  nn0supp  9292  intqfrac2  10390  hashprg  10879  hashfacen  10907  explecnv  11648  grp1inv  13179  rnrhmsubrg  13748  rerestcntop  14718  binom4  15111