Theorem 3eqtr3ri 2268

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

Hypotheses

Ref	Expression
3eqtr3i.1	⊢ 𝐴 = 𝐵
3eqtr3i.2	⊢ 𝐴 = 𝐶
3eqtr3i.3	⊢ 𝐵 = 𝐷

Assertion

Ref	Expression
3eqtr3ri	⊢ 𝐷 = 𝐶

Proof of Theorem 3eqtr3ri

Step	Hyp	Ref	Expression
1		3eqtr3i.3	. 2 ⊢ 𝐵 = 𝐷
2		3eqtr3i.1	. . 3 ⊢ 𝐴 = 𝐵
3		3eqtr3i.2	. . 3 ⊢ 𝐴 = 𝐶
4	2, 3	eqtr3i 2261	. 2 ⊢ 𝐵 = 𝐶
5	1, 4	eqtr3i 2261	1 ⊢ 𝐷 = 𝐶

Syntax hints:   = wceq 1402

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 1500  ax-gen 1502  ax-4 1563  ax-17 1579  ax-ext 2220

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

This theorem is referenced by:  indif2  3475  resdm2  5273  co01  5297  cocnvres  5307  undifdc  7221  1mhlfehlf  9502  rei  11643  resqrexlemover  11754  cos1bnd  12504  m1bits  12705  6gcd4e2  12750  3lcm2e6  12916  karatsuba  13187  ballotfilemth  13259  cosq23lt0  15857  sincos4thpi  15864  sincos6thpi  15866  cosq34lt1  15874