Theorem eqtr3di 2225

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

Syntax hints:   → wi 4   = wceq 1353

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 1447  ax-gen 1449  ax-4 1510  ax-17 1526  ax-ext 2159

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

This theorem is referenced by:  bm2.5ii  4495  resdmdfsn  4950  f0dom0  5409  f1o00  5496  fmpt  5666  fmptsn  5705  resfunexg  5737  mapsn  6689  sbthlemi4  6958  sbthlemi6  6960  pm54.43  7188  prarloclem5  7498  recexprlem1ssl  7631  recexprlem1ssu  7632  iooval2  9914  hashsng  10777  zfz1isolem1  10819  resqrexlemover  11018  isumclim3  11430  algrp1  12045  pythagtriplem1  12264  ressval3d  12530  ressressg  12533  tangtx  14229  coskpi  14239  subctctexmid  14720