Theorem neneor

Description: If two classes are different, a third class must be different of at least one of them. (Contributed by Thierry Arnoux, 8-Aug-2020)

	Ref	Expression
Assertion	neneor	$$⊢A\ne B\to \left(A\ne C\vee B\ne C\right)$$

Proof

Step	Hyp	Ref	Expression
1		eqtr3	$$⊢\left(A=C\wedge B=C\right)\to A=B$$
2	1	necon3ai	$$⊢A\ne B\to \neg \left(A=C\wedge B=C\right)$$
3		neorian	$$⊢\left(A\ne C\vee B\ne C\right)\leftrightarrow \neg \left(A=C\wedge B=C\right)$$
4	2 3	sylibr	$$⊢A\ne B\to \left(A\ne C\vee B\ne C\right)$$