Theorem eqtr3di 2218

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

Syntax hints:   → wi 4   = wceq 1348

This theorem was proved from axioms:  ax-mp 5  ax-1 6  ax-2 7  ax-ia1 105  ax-ia2 106  ax-ia3 107  ax-5 1440  ax-gen 1442  ax-4 1503  ax-17 1519  ax-ext 2152

This theorem depends on definitions:  df-bi 116  df-cleq 2163

This theorem is referenced by:  bm2.5ii  4478  resdmdfsn  4932  f0dom0  5389  f1o00  5475  fmpt  5643  fmptsn  5682  resfunexg  5714  mapsn  6664  sbthlemi4  6933  sbthlemi6  6935  pm54.43  7154  prarloclem5  7449  recexprlem1ssl  7582  recexprlem1ssu  7583  iooval2  9859  hashsng  10720  zfz1isolem1  10762  resqrexlemover  10961  isumclim3  11373  algrp1  11987  pythagtriplem1  12206  tangtx  13474  coskpi  13484  subctctexmid  13956