Theorem et-equeucl

Description: Alternative proof that equality is left-Euclidean, using ax7 directly instead of utility theorems; done for practice. (Contributed by Ender Ting, 21-Dec-2024)

	Ref	Expression
Assertion	et-equeucl	$$⊢x=z\to \left(y=z\to x=y\right)$$

Proof

Step	Hyp	Ref	Expression
1		equid	$$⊢x=x$$
2		ax7	$$⊢x=z\to \left(x=x\to z=x\right)$$
3	2	com12	$$⊢x=x\to \left(x=z\to z=x\right)$$
4	1 3	ax-mp	$$⊢x=z\to z=x$$
5		equid	$$⊢y=y$$
6		ax7	$$⊢y=z\to \left(y=y\to z=y\right)$$
7	6	com12	$$⊢y=y\to \left(y=z\to z=y\right)$$
8	5 7	ax-mp	$$⊢y=z\to z=y$$
9		ax7	$$⊢z=x\to \left(z=y\to x=y\right)$$
10	9	com12	$$⊢z=y\to \left(z=x\to x=y\right)$$
11	8 10	syl	$$⊢y=z\to \left(z=x\to x=y\right)$$
12	11	com12	$$⊢z=x\to \left(y=z\to x=y\right)$$
13	4 12	syl	$$⊢x=z\to \left(y=z\to x=y\right)$$