Theorem eqtr3di 2244

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 2200	. 2 ⊢ 𝐶 = 𝐴
3		eqtr3di.1	. 2 ⊢ (𝜑 → 𝐴 = 𝐵)
4	2, 3	eqtr2id 2242	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 1461  ax-gen 1463  ax-4 1524  ax-17 1540  ax-ext 2178

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

This theorem is referenced by:  bm2.5ii  4532  resdmdfsn  4989  f0dom0  5451  f1o00  5539  fmpt  5712  fmptsn  5751  resfunexg  5783  mapsn  6749  sbthlemi4  7026  sbthlemi6  7028  pm54.43  7257  prarloclem5  7567  recexprlem1ssl  7700  recexprlem1ssu  7701  iooval2  9990  hashsng  10890  zfz1isolem1  10932  resqrexlemover  11175  isumclim3  11588  algrp1  12214  pythagtriplem1  12434  ressbasid  12748  ressval3d  12750  ressressg  12753  tangtx  15074  coskpi  15084  lgsquadlem2  15319  subctctexmid  15645