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  4282  dcextest  4614  relop  4813  funopg  5289  funcnvres  5328  mapsnconst  6750  snexxph  7011  apreap  8608  recextlem1  8672  nn0supp  9295  intqfrac2  10393  hashprg  10882  hashfacen  10910  explecnv  11651  grp1inv  13182  rnrhmsubrg  13751  rerestcntop  14737  rerest  14739  mpomulcn  14745  binom4  15152