Theorem eqtr3di 2225

Description: An equality transitivity deduction. (Contributed by NM, 29-Mar-1998.)

Hypotheses

Ref	Expression
eqtr3di.1	|- ( ph -> A = B )
eqtr3di.2	|- A = C

Assertion

Ref	Expression
eqtr3di	|- ( ph -> B = C )

Proof of Theorem eqtr3di

Step	Hyp	Ref	Expression
1		eqtr3di.2	. . 3 |- A = C
2	1	eqcomi 2181	. 2 |- C = A
3		eqtr3di.1	. 2 |- ( ph -> A = B )
4	2, 3	eqtr2id 2223	1 |- ( ph -> B = C )

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  4496  resdmdfsn  4951  f0dom0  5410  f1o00  5497  fmpt  5667  fmptsn  5706  resfunexg  5738  mapsn  6690  sbthlemi4  6959  sbthlemi6  6961  pm54.43  7189  prarloclem5  7499  recexprlem1ssl  7632  recexprlem1ssu  7633  iooval2  9915  hashsng  10778  zfz1isolem1  10820  resqrexlemover  11019  isumclim3  11431  algrp1  12046  pythagtriplem1  12265  ressval3d  12531  ressressg  12534  tangtx  14262  coskpi  14272  subctctexmid  14753