Theorem equeucl

Equality is a left-Euclidean binary relation. (Right-Euclideanness is stated in [ax-7] .) Curried (exported) form of equtr2. (Contributed by BJ, 11-Apr-2021.)

Conclusion
\( \vdash x' = z' \rightarrow y' = z' \rightarrow x' = y' \)
Proof
equeuclr
com12 _