Theorem eqtr3di 2286

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

This proof depends on syntax axioms:   → wi 4   = wceq 1402

This proof depends on axioms:  ax-mp 5  ax-1 6  ax-2 7  ax-ia1 106  ax-ia2 107  ax-ia3 108  ax-5 1500  ax-gen 1502  ax-4 1563  ax-17 1579  ax-ext 2220

This proof depends on definitions:  df-bi 117  df-cleq 2231

This theorem is used by:  bm2.5ii  4643  resdmdfsn  5106  f0dom0  5586  f1o00  5676  fmpt  5858  fmptsn  5904  resfunexg  5936  fsuppeq  6487  fsuppeqg  6488  mapsnd  6970  mapsn  6972  sbthlemi4  7277  sbthlemi6  7279  2omap  7318  pm54.43  7536  prarloclem5  7867  recexprlem1ssl  8000  recexprlem1ssu  8001  iooval2  10317  hashsng  11237  hashfibc  11283  zfz1isolem1  11292  hashtpglem  11298  resqrexlemover  11776  isumclim3  12190  algrp1  12824  pythagtriplem1  13044  ressbasid  13424  ressval3d  13426  ressressg  13429  tangtx  15939  coskpi  15949  lgsquadlem2  16197  pw1map  17025  subctctexmid  17030