Theorem eqtr2id 2235

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

Syntax hints:   -> wi 4   = wceq 1364

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 1458  ax-gen 1460  ax-4 1521  ax-17 1537  ax-ext 2171

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

This theorem is referenced by:  eqtr3di  2237  opeqsn  4270  dcextest  4598  relop  4795  funopg  5269  funcnvres  5308  mapsnconst  6720  snexxph  6979  apreap  8574  recextlem1  8638  nn0supp  9258  intqfrac2  10350  hashprg  10820  hashfacen  10848  explecnv  11545  grp1inv  13051  rerestcntop  14507  binom4  14854