Theorem eqtr3di 2244

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

Syntax hints:   → wi 4   = wceq 1364

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 1461  ax-gen 1463  ax-4 1524  ax-17 1540  ax-ext 2178

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

This theorem is referenced by:  bm2.5ii  4533  resdmdfsn  4990  f0dom0  5454  f1o00  5542  fmpt  5715  fmptsn  5754  resfunexg  5786  mapsn  6758  sbthlemi4  7035  sbthlemi6  7037  pm54.43  7271  prarloclem5  7586  recexprlem1ssl  7719  recexprlem1ssu  7720  iooval2  10009  hashsng  10909  zfz1isolem1  10951  resqrexlemover  11194  isumclim3  11607  algrp1  12241  pythagtriplem1  12461  ressbasid  12775  ressval3d  12777  ressressg  12780  tangtx  15182  coskpi  15192  lgsquadlem2  15427  2omap  15750  subctctexmid  15755