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$$