Theorem eqtr3di 2279

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 2235	. 2 ⊢ 𝐶 = 𝐴
3		eqtr3di.1	. 2 ⊢ (𝜑 → 𝐴 = 𝐵)
4	2, 3	eqtr2id 2277	1 ⊢ (𝜑 → 𝐵 = 𝐶)

Syntax hints:   → wi 4   = wceq 1397

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 1495  ax-gen 1497  ax-4 1558  ax-17 1574  ax-ext 2213

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

This theorem is referenced by:  bm2.5ii  4594  resdmdfsn  5056  f0dom0  5530  f1o00  5620  fmpt  5797  fmptsn  5842  resfunexg  5874  mapsn  6858  sbthlemi4  7158  sbthlemi6  7160  pm54.43  7394  prarloclem5  7719  recexprlem1ssl  7852  recexprlem1ssu  7853  iooval2  10149  hashsng  11059  zfz1isolem1  11103  resqrexlemover  11570  isumclim3  11983  algrp1  12617  pythagtriplem1  12837  ressbasid  13152  ressval3d  13154  ressressg  13157  tangtx  15561  coskpi  15571  lgsquadlem2  15806  2omap  16594  pw1map  16596  subctctexmid  16601