Theorem sbeqal1

Description: If x = y always implies x = z , then y = z . (Contributed by Andrew Salmon, 2-Jun-2011)

	Ref	Expression
Assertion	sbeqal1	$$⊢\forall x\left(x=y\to x=z\right)\to y=z$$

Proof

Step	Hyp	Ref	Expression
1		sb2	$$⊢\forall x\left(x=y\to x=z\right)\to \left[y/x\right]x=z$$
2		equsb3	$$⊢\left[y/x\right]x=z\leftrightarrow y=z$$
3	1 2	sylib	$$⊢\forall x\left(x=y\to x=z\right)\to y=z$$