This is an inofficial mirror of http://metamath.tirix.org for personal testing of a visualizer extension only.

Metamath Proof Explorer

Theorem equeuclr

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

Ref Expression
Assertion equeuclr ⊢ x = z → y = z → y = x

Proof

Step Hyp Ref Expression
1 equtrr ⊢ z = x → y = z → y = x
2 1 equcoms ⊢ x = z → y = z → y = x