Theorem eqtr2id 2284

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

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:  eqtr3di  2286  opeqsn  4393  dcextest  4728  relop  4930  funopg  5411  funcnvres  5454  mapsnconst  6976  snexxph  7267  apreap  8918  recextlem1  8982  nn0supp  9624  intqfrac2  10771  hashprg  11265  hashfacen  11300  ccatrid  11391  explecnv  12291  grp1inv  13965  rnrhmsubrg  14644  rerestcntop  15750  rerest  15752  mpomulcn  15758  binom4  16180  wlkvtxedg  16770  wlkres  16786