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  3407  resdm2  5160  co01  5184  cocnvres  5194  undifdc  6985  1mhlfehlf  9209  rei  11064  resqrexlemover  11175  cos1bnd  11924  6gcd4e2  12162  3lcm2e6  12328  karatsuba  12599  cosq23lt0  15069  sincos4thpi  15076  sincos6thpi  15078  cosq34lt1  15086