Theorem eqtr2id 2252

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

Syntax hints:   → wi 4   = wceq 1373

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 1471  ax-gen 1473  ax-4 1534  ax-17 1550  ax-ext 2188

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

This theorem is referenced by:  eqtr3di  2254  opeqsn  4304  dcextest  4636  relop  4835  funopg  5313  funcnvres  5355  mapsnconst  6793  snexxph  7066  apreap  8675  recextlem1  8739  nn0supp  9362  intqfrac2  10481  hashprg  10970  hashfacen  10998  ccatrid  11081  explecnv  11886  grp1inv  13509  rnrhmsubrg  14084  rerestcntop  15100  rerest  15102  mpomulcn  15108  binom4  15521