Theorem equeuclr

Description: Commuted version of equeucl (equality is left-Euclidean). (Contributed by BJ, 12-Apr-2021)

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

Proof

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