The Transitivity of Equality

Theorem: ALL(a):ALL(b):ALL(c):[a=b & b=c => a=c]

Proof:

	Suppose...

	1	x=y & y=z
		Premise

	Splitting the above premise...

	2	x=y
		Split, 1

	3	y=z
		Split, 1

	Substituting...

	4	x=z
		Substitute, 2, 3

Applying the Conclusion Rule, we automatically generalize on x, y 
and z using bound variables a, b and c respectively. (User
choses only the names of bound variables.)

5	ALL(a):ALL(b):ALL(c):[a=b & b=c => a=c]
	Conclusion, 1