Theorem eqtr3di 2255

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 2211	. 2 |- C = A
3		eqtr3di.1	. 2 |- ( ph -> A = B )
4	2, 3	eqtr2id 2253	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 1471  ax-gen 1473  ax-4 1534  ax-17 1550  ax-ext 2189

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

This theorem is referenced by:  bm2.5ii  4562  resdmdfsn  5021  f0dom0  5491  f1o00  5580  fmpt  5753  fmptsn  5796  resfunexg  5828  mapsn  6800  sbthlemi4  7088  sbthlemi6  7090  pm54.43  7324  prarloclem5  7648  recexprlem1ssl  7781  recexprlem1ssu  7782  iooval2  10072  hashsng  10980  zfz1isolem1  11022  resqrexlemover  11436  isumclim3  11849  algrp1  12483  pythagtriplem1  12703  ressbasid  13017  ressval3d  13019  ressressg  13022  tangtx  15425  coskpi  15435  lgsquadlem2  15670  2omap  16132  pw1map  16134  subctctexmid  16139