Theorem eqtr2id 2216

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 2215	. 2 |- ( ph -> A = C )
4	3	eqcomd 2176	1 |- ( ph -> C = A )

Syntax hints:   -> wi 4   = wceq 1348

This theorem was proved from axioms:  ax-mp 5  ax-1 6  ax-2 7  ax-ia1 105  ax-ia2 106  ax-ia3 107  ax-5 1440  ax-gen 1442  ax-4 1503  ax-17 1519  ax-ext 2152

This theorem depends on definitions:  df-bi 116  df-cleq 2163

This theorem is referenced by:  eqtr3di  2218  opeqsn  4237  dcextest  4565  relop  4761  funopg  5232  funcnvres  5271  mapsnconst  6672  snexxph  6927  apreap  8506  recextlem1  8569  nn0supp  9187  intqfrac2  10275  hashprg  10743  hashfacen  10771  explecnv  11468  rerestcntop  13344  binom4  13691