Axiom ax-eqeu 327

Description: Equality is Euclidean. Combined with ax-ex 326, this implies that equality is symmetric and transitive.

Assertion

Ref	Expression
ax-eqeu	⊦ (x = y ⊸ (x = z ⊸ y = z))

Detailed syntax breakdown of Axiom ax-eqeu

Step	Hyp	Ref	Expression
1		vx	. . . 4 var x
2	1	nvar 203	. . 3 nilad x
3		vy	. . . 4 var y
4	3	nvar 203	. . 3 nilad y
5	2, 4	weq 246	. 2 wff x = y
6		vz	. . . . 5 var z
7	6	nvar 203	. . . 4 nilad z
8	2, 7	weq 246	. . 3 wff x = z
9	4, 7	weq 246	. . 3 wff y = z
10	8, 9	wli 61	. 2 wff (x = z ⊸ y = z)
11	5, 10	wli 61	1 wff (x = y ⊸ (x = z ⊸ y = z))

This axiom is referenced by: (None)