Theorem eqtr2id 2280

Description: An equality transitivity deduction. (Contributed by NM, 29-Mar-1998.)

Hypotheses

Ref	Expression
eqtr2id.1	|- A = B
eqtr2id.2	|- ( ph -> B = C )

Assertion

Ref	Expression
eqtr2id	|- ( ph -> C = A )

Proof of Theorem eqtr2id

Step	Hyp	Ref	Expression
1		eqtr2id.1	. . 3 |- A = B
2		eqtr2id.2	. . 3 |- ( ph -> B = C )
3	1, 2	eqtrid 2279	. 2 |- ( ph -> A = C )
4	3	eqcomd 2240	1 |- ( ph -> C = A )

Syntax hints:   -> wi 4   = wceq 1398

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 1496  ax-gen 1498  ax-4 1559  ax-17 1575  ax-ext 2216

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

This theorem is referenced by:  eqtr3di  2282  opeqsn  4374  dcextest  4708  relop  4910  funopg  5391  funcnvres  5434  mapsnconst  6942  snexxph  7233  apreap  8879  recextlem1  8943  nn0supp  9572  intqfrac2  10708  hashprg  11201  hashfacen  11236  ccatrid  11323  explecnv  12220  grp1inv  13866  rnrhmsubrg  14502  rerestcntop  15553  rerest  15555  mpomulcn  15561  binom4  15974  wlkvtxedg  16488  wlkres  16504