Theorem pm13.181

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

	Ref	Expression
Assertion	pm13.181	|- ( ( A = B /\ B =/= C ) -> A =/= C )

Proof

Step	Hyp	Ref	Expression
1		eqcom	|- ( A = B <-> B = A )
2		pm13.18	|- ( ( B = A /\ B =/= C ) -> A =/= C )
3	1 2	sylanb	|- ( ( A = B /\ B =/= C ) -> A =/= C )