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 ) )