Theorem nbrne1

Description: Two classes are different if they don't have the same relationship to a third class. (Contributed by NM, 3-Jun-2012)

	Ref	Expression
Assertion	nbrne1	$$⊢\left(ARB\wedge \neg ARC\right)\to B\ne C$$

Proof

Step	Hyp	Ref	Expression
1		breq2	$$⊢B=C\to \left(ARB\leftrightarrow ARC\right)$$
2	1	biimpcd	$$⊢ARB\to \left(B=C\to ARC\right)$$
3	2	necon3bd	$$⊢ARB\to \left(\neg ARC\to B\ne C\right)$$
4	3	imp	$$⊢\left(ARB\wedge \neg ARC\right)\to B\ne C$$