Theorem eqtr3di 2286

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

This proof depends on syntax axioms:   -> wi 4   = wceq 1402

This proof depends on axioms:  ax-mp 5  ax-1 6  ax-2 7  ax-ia1 106  ax-ia2 107  ax-ia3 108  ax-5 1500  ax-gen 1502  ax-4 1563  ax-17 1579  ax-ext 2220

This proof depends on definitions:  df-bi 117  df-cleq 2231

This theorem is used by:  bm2.5ii  4643  resdmdfsn  5106  f0dom0  5586  f1o00  5676  fmpt  5858  fmptsn  5904  resfunexg  5936  fsuppeq  6487  fsuppeqg  6488  mapsnd  6970  mapsn  6972  sbthlemi4  7277  sbthlemi6  7279  2omap  7319  pm54.43  7537  prarloclem5  7868  recexprlem1ssl  8001  recexprlem1ssu  8002  iooval2  10328  hashsng  11253  hashfibc  11299  zfz1isolem1  11308  hashtpglem  11314  resqrexlemover  11792  isumclim3  12209  algrp1  12843  pythagtriplem1  13067  ressbasid  13477  ressval3d  13479  ressressg  13482  tangtx  16031  coskpi  16041  chtqub  16257  bposlem6  16277  lgsquadlem2  16363  pw1map  17191  subctctexmid  17196