Theorem equtr

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

	Ref	Expression
Assertion	equtr	⊢ ( 𝑥 = 𝑦 → ( 𝑦 = 𝑧 → 𝑥 = 𝑧 ) )

Proof

Step	Hyp	Ref	Expression
1		ax7	⊢ ( 𝑦 = 𝑥 → ( 𝑦 = 𝑧 → 𝑥 = 𝑧 ) )
2	1	equcoms	⊢ ( 𝑥 = 𝑦 → ( 𝑦 = 𝑧 → 𝑥 = 𝑧 ) )