Theorem sbeqal1i

Description: Suppose you know x = y implies x = z , assuming x and z are distinct. Then, y = z . (Contributed by Andrew Salmon, 3-Jun-2011)

	Ref	Expression
Hypothesis	sbeqal1i.1	|- ( x = y -> x = z )
Assertion	sbeqal1i	|- y = z

Proof

Step	Hyp	Ref	Expression
1		sbeqal1i.1	|- ( x = y -> x = z )
2		sbeqal1	|- ( A. x ( x = y -> x = z ) -> y = z )
3	2 1	mpg	|- y = z