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  4544  resdmdfsn  5002  f0dom0  5469  f1o00  5557  fmpt  5730  fmptsn  5773  resfunexg  5805  mapsn  6777  sbthlemi4  7062  sbthlemi6  7064  pm54.43  7298  prarloclem5  7613  recexprlem1ssl  7746  recexprlem1ssu  7747  iooval2  10037  hashsng  10943  zfz1isolem1  10985  resqrexlemover  11321  isumclim3  11734  algrp1  12368  pythagtriplem1  12588  ressbasid  12902  ressval3d  12904  ressressg  12907  tangtx  15310  coskpi  15320  lgsquadlem2  15555  2omap  15932  subctctexmid  15937