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 -> ( y = z -> x = y ) )

Proof

Step	Hyp	Ref	Expression
1		equid	|- x = x
2		ax7	|- ( x = z -> ( x = x -> z = x ) )
3	2	com12	|- ( x = x -> ( x = z -> z = x ) )
4	1 3	ax-mp	|- ( x = z -> z = x )
5		equid	|- y = y
6		ax7	|- ( y = z -> ( y = y -> z = y ) )
7	6	com12	|- ( y = y -> ( y = z -> z = y ) )
8	5 7	ax-mp	|- ( y = z -> z = y )
9		ax7	|- ( z = x -> ( z = y -> x = y ) )
10	9	com12	|- ( z = y -> ( z = x -> x = y ) )
11	8 10	syl	|- ( y = z -> ( z = x -> x = y ) )
12	11	com12	|- ( z = x -> ( y = z -> x = y ) )
13	4 12	syl	|- ( x = z -> ( y = z -> x = y ) )