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 ⊢ (𝜑 → 𝐵 = 𝐶)

Syntax hints:   → wi 4   = wceq 1402

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 1500  ax-gen 1502  ax-4 1563  ax-17 1579  ax-ext 2220

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

This theorem is referenced by:  bm2.5ii  4638  resdmdfsn  5101  f0dom0  5581  f1o00  5671  fmpt  5849  fmptsn  5895  resfunexg  5927  fsuppeq  6477  fsuppeqg  6478  mapsnd  6960  mapsn  6962  sbthlemi4  7267  sbthlemi6  7269  2omap  7308  pm54.43  7526  prarloclem5  7857  recexprlem1ssl  7990  recexprlem1ssu  7991  iooval2  10296  hashsng  11215  hashfibc  11261  zfz1isolem1  11270  hashtpglem  11276  resqrexlemover  11754  isumclim3  12168  algrp1  12802  pythagtriplem1  13022  ressbasid  13401  ressval3d  13403  ressressg  13406  tangtx  15862  coskpi  15872  lgsquadlem2  16111  pw1map  16939  subctctexmid  16944