Theorem eqtr2id 2253

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

Syntax hints:   -> wi 4   = wceq 1373

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 1471  ax-gen 1473  ax-4 1534  ax-17 1550  ax-ext 2189

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

This theorem is referenced by:  eqtr3di  2255  opeqsn  4315  dcextest  4647  relop  4846  funopg  5324  funcnvres  5366  mapsnconst  6804  snexxph  7078  apreap  8695  recextlem1  8759  nn0supp  9382  intqfrac2  10501  hashprg  10990  hashfacen  11018  ccatrid  11101  explecnv  11931  grp1inv  13554  rnrhmsubrg  14129  rerestcntop  15145  rerest  15147  mpomulcn  15153  binom4  15566