Theorem eqtr3di 2225

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

Syntax hints:   → wi 4   = wceq 1353

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 1447  ax-gen 1449  ax-4 1510  ax-17 1526  ax-ext 2159

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

This theorem is referenced by:  bm2.5ii  4497  resdmdfsn  4952  f0dom0  5411  f1o00  5498  fmpt  5668  fmptsn  5707  resfunexg  5739  mapsn  6692  sbthlemi4  6961  sbthlemi6  6963  pm54.43  7191  prarloclem5  7501  recexprlem1ssl  7634  recexprlem1ssu  7635  iooval2  9917  hashsng  10780  zfz1isolem1  10822  resqrexlemover  11021  isumclim3  11433  algrp1  12048  pythagtriplem1  12267  ressval3d  12533  ressressg  12536  tangtx  14298  coskpi  14308  subctctexmid  14789