Theorem 3eqtr3ri 2226

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 2219	. 2 ⊢ 𝐵 = 𝐶
5	1, 4	eqtr3i 2219	1 ⊢ 𝐷 = 𝐶

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  9228  rei  11083  resqrexlemover  11194  cos1bnd  11943  m1bits  12144  6gcd4e2  12189  3lcm2e6  12355  karatsuba  12626  cosq23lt0  15177  sincos4thpi  15184  sincos6thpi  15186  cosq34lt1  15194