Theorem
equeuclr
Commuted version of
equeucl
(equality is left-Euclidean). (Contributed by BJ, 12-Apr-2021.)
Conclusion
\( \vdash x' = z' \rightarrow y' = z' \rightarrow y' = x' \)
Proof
equtrr
equcoms
_
This is the content in the right pane.