Theorem neeqtrd

Description: Substitution of equal classes into an inequality. (Contributed by NM, 4-Jul-2012)

	Ref	Expression
Hypotheses	neeqtrd.1	$$⊢\phi \to A\ne B$$
	neeqtrd.2	$$⊢\phi \to B=C$$
Assertion	neeqtrd	$$⊢\phi \to A\ne C$$

Proof

Step	Hyp	Ref	Expression
1		neeqtrd.1	$$⊢\phi \to A\ne B$$
2		neeqtrd.2	$$⊢\phi \to B=C$$
3	2	neeq2d	$$⊢\phi \to \left(A\ne B\leftrightarrow A\ne C\right)$$
4	1 3	mpbid	$$⊢\phi \to A\ne C$$