Theorem pm13.181

Description: Theorem *13.181 in WhiteheadRussell p. 178. (Contributed by Andrew Salmon, 3-Jun-2011)

	Ref	Expression
Assertion	pm13.181	$$⊢\left(A=B\wedge B\ne C\right)\to A\ne C$$

Proof

Step	Hyp	Ref	Expression
1		eqcom	$$⊢A=B\leftrightarrow B=A$$
2		pm13.18	$$⊢\left(B=A\wedge B\ne C\right)\to A\ne C$$
3	1 2	sylanb	$$⊢\left(A=B\wedge B\ne C\right)\to A\ne C$$