Theorem eqtr3di 2279

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

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

This theorem is referenced by:  bm2.5ii  4600  resdmdfsn  5062  f0dom0  5539  f1o00  5629  fmpt  5805  fmptsn  5851  resfunexg  5883  fsuppeq  6425  fsuppeqg  6426  mapsn  6902  sbthlemi4  7202  sbthlemi6  7204  pm54.43  7438  prarloclem5  7763  recexprlem1ssl  7896  recexprlem1ssu  7897  iooval2  10194  hashsng  11106  zfz1isolem1  11150  hashtpglem  11156  resqrexlemover  11633  isumclim3  12047  algrp1  12681  pythagtriplem1  12901  ressbasid  13216  ressval3d  13218  ressressg  13221  tangtx  15632  coskpi  15642  lgsquadlem2  15880  2omap  16698  pw1map  16700  subctctexmid  16705