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 ⊢ 𝐷 = 𝐶

This proof depends on syntax axioms:   = wceq 1402

This proof depends on 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 proof depends on definitions:  df-bi 117  df-cleq 2231

This theorem is used by:  indif2  3475  resdm2  5278  co01  5302  cocnvres  5312  undifdc  7231  1mhlfehlf  9528  rei  11681  resqrexlemover  11792  cos1bnd  12545  m1bits  12746  6gcd4e2  12791  3lcm2e6  12958  karatsuba  13233  ballotfilemth  13333  cosq23lt0  16026  sincos4thpi  16033  sincos6thpi  16035  cosq34lt1  16043  cht3  16238  bclbnd  16268  bposlem8  16279