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\to x=z$$
Assertion	sbeqal1i	$$⊢y=z$$

Proof

Step	Hyp	Ref	Expression
1		sbeqal1i.1	$$⊢x=y\to x=z$$
2		sbeqal1	$$⊢\forall x\left(x=y\to x=z\right)\to y=z$$
3	2 1	mpg	$$⊢y=z$$