Theorem 3eqtr3ri 2235

Description: An inference from three chained equalities. (Contributed by NM, 15-Aug-2004.)

Hypotheses

Ref	Expression
3eqtr3i.1	|- A = B
3eqtr3i.2	|- A = C
3eqtr3i.3	|- B = D

Assertion

Ref	Expression
3eqtr3ri	|- D = C

Proof of Theorem 3eqtr3ri

Step	Hyp	Ref	Expression
1		3eqtr3i.3	. 2 |- B = D
2		3eqtr3i.1	. . 3 |- A = B
3		3eqtr3i.2	. . 3 |- A = C
4	2, 3	eqtr3i 2228	. 2 |- B = C
5	1, 4	eqtr3i 2228	1 |- D = C

Syntax hints:   = 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 1470  ax-gen 1472  ax-4 1533  ax-17 1549  ax-ext 2187

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

This theorem is referenced by:  indif2  3417  resdm2  5173  co01  5197  cocnvres  5207  undifdc  7021  1mhlfehlf  9255  rei  11210  resqrexlemover  11321  cos1bnd  12070  m1bits  12271  6gcd4e2  12316  3lcm2e6  12482  karatsuba  12753  cosq23lt0  15305  sincos4thpi  15312  sincos6thpi  15314  cosq34lt1  15322