Theorem eqtr3di 2277

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

Syntax hints:   → wi 4   = wceq 1395

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 1493  ax-gen 1495  ax-4 1556  ax-17 1572  ax-ext 2211

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

This theorem is referenced by:  bm2.5ii  4587  resdmdfsn  5047  f0dom0  5518  f1o00  5607  fmpt  5784  fmptsn  5827  resfunexg  5859  mapsn  6835  sbthlemi4  7123  sbthlemi6  7125  pm54.43  7359  prarloclem5  7683  recexprlem1ssl  7816  recexprlem1ssu  7817  iooval2  10107  hashsng  11015  zfz1isolem1  11057  resqrexlemover  11516  isumclim3  11929  algrp1  12563  pythagtriplem1  12783  ressbasid  13098  ressval3d  13100  ressressg  13103  tangtx  15506  coskpi  15516  lgsquadlem2  15751  2omap  16318  pw1map  16320  subctctexmid  16325