Theorem eqtr2id 2277

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 2276	. 2 |- ( ph -> A = C )
4	3	eqcomd 2237	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 2213

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

This theorem is referenced by:  eqtr3di  2279  opeqsn  4351  dcextest  4685  relop  4886  funopg  5367  funcnvres  5410  mapsnconst  6906  snexxph  7192  apreap  8826  recextlem1  8890  nn0supp  9515  intqfrac2  10644  hashprg  11135  hashfacen  11163  ccatrid  11250  explecnv  12146  grp1inv  13770  rnrhmsubrg  14347  rerestcntop  15369  rerest  15371  mpomulcn  15377  binom4  15790  wlkvtxedg  16304  wlkres  16320