Theorem eqtr3di 2277

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

Syntax hints:   -> wi 4   = wceq 1395

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 1493  ax-gen 1495  ax-4 1556  ax-17 1572  ax-ext 2211

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

This theorem is referenced by:  bm2.5ii  4588  resdmdfsn  5048  f0dom0  5519  f1o00  5608  fmpt  5785  fmptsn  5828  resfunexg  5860  mapsn  6837  sbthlemi4  7127  sbthlemi6  7129  pm54.43  7363  prarloclem5  7687  recexprlem1ssl  7820  recexprlem1ssu  7821  iooval2  10111  hashsng  11020  zfz1isolem1  11062  resqrexlemover  11521  isumclim3  11934  algrp1  12568  pythagtriplem1  12788  ressbasid  13103  ressval3d  13105  ressressg  13108  tangtx  15512  coskpi  15522  lgsquadlem2  15757  2omap  16359  pw1map  16361  subctctexmid  16366