Theorem eqtr3di 2244

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 2200	. 2 |- C = A
3		eqtr3di.1	. 2 |- ( ph -> A = B )
4	2, 3	eqtr2id 2242	1 |- ( ph -> B = C )

Syntax hints:   -> wi 4   = wceq 1364

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 1461  ax-gen 1463  ax-4 1524  ax-17 1540  ax-ext 2178

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

This theorem is referenced by:  bm2.5ii  4533  resdmdfsn  4990  f0dom0  5452  f1o00  5540  fmpt  5713  fmptsn  5752  resfunexg  5784  mapsn  6750  sbthlemi4  7027  sbthlemi6  7029  pm54.43  7259  prarloclem5  7569  recexprlem1ssl  7702  recexprlem1ssu  7703  iooval2  9992  hashsng  10892  zfz1isolem1  10934  resqrexlemover  11177  isumclim3  11590  algrp1  12224  pythagtriplem1  12444  ressbasid  12758  ressval3d  12760  ressressg  12763  tangtx  15084  coskpi  15094  lgsquadlem2  15329  subctctexmid  15655