Theorem 3eqtr3ri 2226

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 2219	. 2 |- B = C
5	1, 4	eqtr3i 2219	1 |- D = C

Syntax hints:   = wceq 1364

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 1461  ax-gen 1463  ax-4 1524  ax-17 1540  ax-ext 2178

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

This theorem is referenced by:  indif2  3408  resdm2  5161  co01  5185  cocnvres  5195  undifdc  6994  1mhlfehlf  9226  rei  11081  resqrexlemover  11192  cos1bnd  11941  m1bits  12142  6gcd4e2  12187  3lcm2e6  12353  karatsuba  12624  cosq23lt0  15153  sincos4thpi  15160  sincos6thpi  15162  cosq34lt1  15170