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  5843  resfunexg  5875  mapsn  6859  sbthlemi4  7159  sbthlemi6  7161  pm54.43  7395  prarloclem5  7720  recexprlem1ssl  7853  recexprlem1ssu  7854  iooval2  10150  hashsng  11061  zfz1isolem1  11105  hashtpglem  11111  resqrexlemover  11588  isumclim3  12002  algrp1  12636  pythagtriplem1  12856  ressbasid  13171  ressval3d  13173  ressressg  13176  tangtx  15581  coskpi  15591  lgsquadlem2  15826  2omap  16645  pw1map  16647  subctctexmid  16652