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  7318  pm54.43  7536  prarloclem5  7867  recexprlem1ssl  8000  recexprlem1ssu  8001  iooval2  10327  hashsng  11251  hashfibc  11297  zfz1isolem1  11306  hashtpglem  11312  resqrexlemover  11790  isumclim3  12206  algrp1  12840  pythagtriplem1  13064  ressbasid  13473  ressval3d  13475  ressressg  13478  tangtx  15989  coskpi  15999  lgsquadlem2  16295  pw1map  17123  subctctexmid  17128