Theorem eqtr3di 2280

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

Syntax hints:   → wi 4   = wceq 1398

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 1496  ax-gen 1498  ax-4 1559  ax-17 1575  ax-ext 2214

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

This theorem is referenced by:  bm2.5ii  4618  resdmdfsn  5081  f0dom0  5561  f1o00  5651  fmpt  5827  fmptsn  5873  resfunexg  5905  fsuppeq  6447  fsuppeqg  6448  mapsnd  6923  mapsn  6925  sbthlemi4  7230  sbthlemi6  7232  2omap  7269  pm54.43  7487  prarloclem5  7815  recexprlem1ssl  7948  recexprlem1ssu  7949  iooval2  10248  hashsng  11161  hashfibc  11207  zfz1isolem1  11212  hashtpglem  11218  resqrexlemover  11695  isumclim3  12109  algrp1  12743  pythagtriplem1  12963  ressbasid  13283  ressval3d  13285  ressressg  13288  tangtx  15703  coskpi  15713  lgsquadlem2  15951  pw1map  16769  subctctexmid  16774