Theorem ne3anior

Description: A De Morgan's law for inequality. (Contributed by NM, 30-Sep-2013)

	Ref	Expression
Assertion	ne3anior	$$⊢\left(A\ne B\wedge C\ne D\wedge E\ne F\right)\leftrightarrow \neg \left(A=B\vee C=D\vee E=F\right)$$

Proof

Step	Hyp	Ref	Expression
1		3anor	$$⊢\left(A\ne B\wedge C\ne D\wedge E\ne F\right)\leftrightarrow \neg \left(\neg A\ne B\vee \neg C\ne D\vee \neg E\ne F\right)$$
2		nne	$$⊢\neg A\ne B\leftrightarrow A=B$$
3		nne	$$⊢\neg C\ne D\leftrightarrow C=D$$
4		nne	$$⊢\neg E\ne F\leftrightarrow E=F$$
5	2 3 4	3orbi123i	$$⊢\left(\neg A\ne B\vee \neg C\ne D\vee \neg E\ne F\right)\leftrightarrow \left(A=B\vee C=D\vee E=F\right)$$
6	1 5	xchbinx	$$⊢\left(A\ne B\wedge C\ne D\wedge E\ne F\right)\leftrightarrow \neg \left(A=B\vee C=D\vee E=F\right)$$