Theorem eqtr3di 2252

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

Syntax hints:   → wi 4   = wceq 1372

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 1469  ax-gen 1471  ax-4 1532  ax-17 1548  ax-ext 2186

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

This theorem is referenced by:  bm2.5ii  4542  resdmdfsn  4999  f0dom0  5463  f1o00  5551  fmpt  5724  fmptsn  5763  resfunexg  5795  mapsn  6767  sbthlemi4  7044  sbthlemi6  7046  pm54.43  7280  prarloclem5  7595  recexprlem1ssl  7728  recexprlem1ssu  7729  iooval2  10019  hashsng  10924  zfz1isolem1  10966  resqrexlemover  11240  isumclim3  11653  algrp1  12287  pythagtriplem1  12507  ressbasid  12821  ressval3d  12823  ressressg  12826  tangtx  15228  coskpi  15238  lgsquadlem2  15473  2omap  15796  subctctexmid  15801