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  8915  recextlem1  8979  nn0supp  9619  intqfrac2  10756  hashprg  11249  hashfacen  11284  ccatrid  11375  explecnv  12272  grp1inv  13912  rnrhmsubrg  14560  rerestcntop  15659  rerest  15661  mpomulcn  15667  binom4  16081  wlkvtxedg  16604  wlkres  16620