Metamath Proof Explorer
Description: Commuted version of equeucl (equality is leftEuclidean). (Contributed by BJ, 12Apr2021)


Ref 
Expression 

Assertion 
equeuclr 
$${\u22a2}{x}={z}\to \left({y}={z}\to {y}={x}\right)$$ 
Proof
Step 
Hyp 
Ref 
Expression 
1 

equtrr 
$${\u22a2}{z}={x}\to \left({y}={z}\to {y}={x}\right)$$ 
2 
1

equcoms 
$${\u22a2}{x}={z}\to \left({y}={z}\to {y}={x}\right)$$ 