Theorem pm13.181OLD

Description: Obsolete version of pm13.181 as of 30-Oct-2024. (Contributed by Andrew Salmon, 3-Jun-2011) (New usage is discouraged.) (Proof modification is discouraged.)

	Ref	Expression
Assertion	pm13.181OLD	$$⊢\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$$