Theorem eqtr3di 2218

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

Syntax hints:   → wi 4   = wceq 1348

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 1440  ax-gen 1442  ax-4 1503  ax-17 1519  ax-ext 2152

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

This theorem is referenced by:  bm2.5ii  4480  resdmdfsn  4934  f0dom0  5391  f1o00  5477  fmpt  5646  fmptsn  5685  resfunexg  5717  mapsn  6668  sbthlemi4  6937  sbthlemi6  6939  pm54.43  7167  prarloclem5  7462  recexprlem1ssl  7595  recexprlem1ssu  7596  iooval2  9872  hashsng  10733  zfz1isolem1  10775  resqrexlemover  10974  isumclim3  11386  algrp1  12000  pythagtriplem1  12219  tangtx  13553  coskpi  13563  subctctexmid  14034