Theorem neeqtrri

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

	Ref	Expression
Hypotheses	neeqtrr.1	|- A =/= B
	neeqtrr.2	|- C = B
Assertion	neeqtrri	|- A =/= C

Proof

Step	Hyp	Ref	Expression
1		neeqtrr.1	|- A =/= B
2		neeqtrr.2	|- C = B
3	2	eqcomi	|- B = C
4	1 3	neeqtri	|- A =/= C