Theorem eqtr3di 2241

Description: An equality transitivity deduction. (Contributed by NM, 29-Mar-1998.)

Hypotheses

Ref	Expression
eqtr3di.1	⊢ (𝜑 → 𝐴 = 𝐵)
eqtr3di.2	⊢ 𝐴 = 𝐶

Assertion

Ref	Expression
eqtr3di	⊢ (𝜑 → 𝐵 = 𝐶)

Proof of Theorem eqtr3di

Step	Hyp	Ref	Expression
1		eqtr3di.2	. . 3 ⊢ 𝐴 = 𝐶
2	1	eqcomi 2197	. 2 ⊢ 𝐶 = 𝐴
3		eqtr3di.1	. 2 ⊢ (𝜑 → 𝐴 = 𝐵)
4	2, 3	eqtr2id 2239	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:  bm2.5ii  4528  resdmdfsn  4985  f0dom0  5447  f1o00  5535  fmpt  5708  fmptsn  5747  resfunexg  5779  mapsn  6744  sbthlemi4  7019  sbthlemi6  7021  pm54.43  7250  prarloclem5  7560  recexprlem1ssl  7693  recexprlem1ssu  7694  iooval2  9981  hashsng  10869  zfz1isolem1  10911  resqrexlemover  11154  isumclim3  11566  algrp1  12184  pythagtriplem1  12403  ressbasid  12688  ressval3d  12690  ressressg  12693  tangtx  14973  coskpi  14983  subctctexmid  15491