Theorem eqtr3di 2241

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 2197	. 2 |- C = A
3		eqtr3di.1	. 2 |- ( ph -> A = B )
4	2, 3	eqtr2id 2239	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 1458  ax-gen 1460  ax-4 1521  ax-17 1537  ax-ext 2175

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

This theorem is referenced by:  bm2.5ii  4529  resdmdfsn  4986  f0dom0  5448  f1o00  5536  fmpt  5709  fmptsn  5748  resfunexg  5780  mapsn  6746  sbthlemi4  7021  sbthlemi6  7023  pm54.43  7252  prarloclem5  7562  recexprlem1ssl  7695  recexprlem1ssu  7696  iooval2  9984  hashsng  10872  zfz1isolem1  10914  resqrexlemover  11157  isumclim3  11569  algrp1  12187  pythagtriplem1  12406  ressbasid  12691  ressval3d  12693  ressressg  12696  tangtx  15014  coskpi  15024  lgsquadlem2  15235  subctctexmid  15561