Theorem eqtr3di 2213

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

Syntax hints:   → wi 4   = wceq 1343

This theorem was proved from axioms:  ax-mp 5  ax-1 6  ax-2 7  ax-ia1 105  ax-ia2 106  ax-ia3 107  ax-5 1435  ax-gen 1437  ax-4 1498  ax-17 1514  ax-ext 2147

This theorem depends on definitions:  df-bi 116  df-cleq 2158

This theorem is referenced by:  bm2.5ii  4472  resdmdfsn  4926  f0dom0  5380  f1o00  5466  fmpt  5634  fmptsn  5673  resfunexg  5705  mapsn  6652  sbthlemi4  6921  sbthlemi6  6923  pm54.43  7142  prarloclem5  7437  recexprlem1ssl  7570  recexprlem1ssu  7571  iooval2  9847  hashsng  10707  zfz1isolem1  10749  resqrexlemover  10948  isumclim3  11360  algrp1  11974  pythagtriplem1  12193  tangtx  13359  coskpi  13369  subctctexmid  13841