Theorem equeuclr

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

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

Proof

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