Theorem equtr

Description: A transitive law for equality. (Contributed by NM, 23-Aug-1993)

	Ref	Expression
Assertion	equtr	$$⊢x=y\to \left(y=z\to x=z\right)$$

Proof

Step	Hyp	Ref	Expression
1		ax7	$$⊢y=x\to \left(y=z\to x=z\right)$$
2	1	equcoms	$$⊢x=y\to \left(y=z\to x=z\right)$$