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  6974  mapsn  6976  sbthlemi4  7282  sbthlemi6  7284  2omap  7324  pm54.43  7542  prarloclem5  7873  recexprlem1ssl  8006  recexprlem1ssu  8007  iooval2  10334  hashsng  11259  hashfibc  11305  zfz1isolem1  11314  hashtpglem  11320  resqrexlemover  11798  isumclim3  12215  algrp1  12849  pythagtriplem1  13073  ressbasid  13483  ressval3d  13485  ressressg  13488  tangtx  16065  coskpi  16075  chtqub  16296  bposlem6  16316  lgsquadlem2  16402  pw1map  17230  subctctexmid  17235