Theorem 3eqtri

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

	Ref	Expression
Hypotheses	3eqtri.1	|- A = B
	3eqtri.2	|- B = C
	3eqtri.3	|- C = D
Assertion	3eqtri	|- A = D

Proof

Step	Hyp	Ref	Expression
1		3eqtri.1	|- A = B
2		3eqtri.2	|- B = C
3		3eqtri.3	|- C = D
4	2 3	eqtri	|- B = D
5	1 4	eqtri	|- A = D