Theorem eqtr3di 2254

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

Syntax hints:   → wi 4   = wceq 1373

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 1471  ax-gen 1473  ax-4 1534  ax-17 1550  ax-ext 2188

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

This theorem is referenced by:  bm2.5ii  4552  resdmdfsn  5011  f0dom0  5481  f1o00  5570  fmpt  5743  fmptsn  5786  resfunexg  5818  mapsn  6790  sbthlemi4  7077  sbthlemi6  7079  pm54.43  7313  prarloclem5  7633  recexprlem1ssl  7766  recexprlem1ssu  7767  iooval2  10057  hashsng  10965  zfz1isolem1  11007  resqrexlemover  11396  isumclim3  11809  algrp1  12443  pythagtriplem1  12663  ressbasid  12977  ressval3d  12979  ressressg  12982  tangtx  15385  coskpi  15395  lgsquadlem2  15630  2omap  16071  pw1map  16073  subctctexmid  16078