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  4645  resdmdfsn  5109  f0dom0  5589  f1o00  5679  fmpt  5861  fmptsn  5907  resfunexg  5939  fsuppeq  6491  fsuppeqg  6492  mapsnd  6976  mapsn  6978  sbthlemi4  7284  sbthlemi6  7286  2omap  7324  pm54.43  7542  prarloclem5  7873  recexprlem1ssl  8006  recexprlem1ssu  8007  iooval2  10333  hashsng  11258  hashfibc  11304  zfz1isolem1  11313  hashtpglem  11319  resqrexlemover  11797  isumclim3  12214  algrp1  12848  pythagtriplem1  13072  ressbasid  13482  ressval3d  13484  ressressg  13487  tangtx  16082  coskpi  16092  chtqub  16313  bposlem6  16333  lgsquadlem2  16419  pw1map  17247  subctctexmid  17252