Theorem eqtr3di 2282

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

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

This theorem is referenced by:  bm2.5ii  4623  resdmdfsn  5086  f0dom0  5566  f1o00  5656  fmpt  5832  fmptsn  5878  resfunexg  5910  fsuppeq  6460  fsuppeqg  6461  mapsnd  6936  mapsn  6938  sbthlemi4  7243  sbthlemi6  7245  2omap  7282  pm54.43  7500  prarloclem5  7831  recexprlem1ssl  7964  recexprlem1ssu  7965  iooval2  10267  hashsng  11186  hashfibc  11232  zfz1isolem1  11237  hashtpglem  11243  resqrexlemover  11720  isumclim3  12134  algrp1  12768  pythagtriplem1  12988  ressbasid  13367  ressval3d  13369  ressressg  13372  tangtx  15829  coskpi  15839  lgsquadlem2  16077  pw1map  16895  subctctexmid  16900