Theorem eqtr3di 2253

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

Syntax hints:   -> wi 4   = wceq 1373

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 1470  ax-gen 1472  ax-4 1533  ax-17 1549  ax-ext 2187

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

This theorem is referenced by:  bm2.5ii  4545  resdmdfsn  5003  f0dom0  5471  f1o00  5559  fmpt  5732  fmptsn  5775  resfunexg  5807  mapsn  6779  sbthlemi4  7064  sbthlemi6  7066  pm54.43  7300  prarloclem5  7615  recexprlem1ssl  7748  recexprlem1ssu  7749  iooval2  10039  hashsng  10945  zfz1isolem1  10987  resqrexlemover  11354  isumclim3  11767  algrp1  12401  pythagtriplem1  12621  ressbasid  12935  ressval3d  12937  ressressg  12940  tangtx  15343  coskpi  15353  lgsquadlem2  15588  2omap  15969  subctctexmid  15974