Theorem otthne

Description: Contrapositive of the ordered triple theorem. (Contributed by Scott Fenton, 31-Jan-2025)

	Ref	Expression
Hypotheses	otthne.1	$$⊢A\in \mathrm{V}$$
	otthne.2	$$⊢B\in \mathrm{V}$$
	otthne.3	$$⊢C\in \mathrm{V}$$
Assertion	otthne	$$⊢⟨A,B,C⟩\ne ⟨D,E,F⟩\leftrightarrow \left(A\ne D\vee B\ne E\vee C\ne F\right)$$

Proof

Step	Hyp	Ref	Expression
1		otthne.1	$$⊢A\in \mathrm{V}$$
2		otthne.2	$$⊢B\in \mathrm{V}$$
3		otthne.3	$$⊢C\in \mathrm{V}$$
4	1 2 3	otth	$$⊢⟨A,B,C⟩=⟨D,E,F⟩\leftrightarrow \left(A=D\wedge B=E\wedge C=F\right)$$
5	4	notbii	$$⊢\neg ⟨A,B,C⟩=⟨D,E,F⟩\leftrightarrow \neg \left(A=D\wedge B=E\wedge C=F\right)$$
6		3ianor	$$⊢\neg \left(A=D\wedge B=E\wedge C=F\right)\leftrightarrow \left(\neg A=D\vee \neg B=E\vee \neg C=F\right)$$
7	5 6	bitri	$$⊢\neg ⟨A,B,C⟩=⟨D,E,F⟩\leftrightarrow \left(\neg A=D\vee \neg B=E\vee \neg C=F\right)$$
8		df-ne	$$⊢⟨A,B,C⟩\ne ⟨D,E,F⟩\leftrightarrow \neg ⟨A,B,C⟩=⟨D,E,F⟩$$
9		df-ne	$$⊢A\ne D\leftrightarrow \neg A=D$$
10		df-ne	$$⊢B\ne E\leftrightarrow \neg B=E$$
11		df-ne	$$⊢C\ne F\leftrightarrow \neg C=F$$
12	9 10 11	3orbi123i	$$⊢\left(A\ne D\vee B\ne E\vee C\ne F\right)\leftrightarrow \left(\neg A=D\vee \neg B=E\vee \neg C=F\right)$$
13	7 8 12	3bitr4i	$$⊢⟨A,B,C⟩\ne ⟨D,E,F⟩\leftrightarrow \left(A\ne D\vee B\ne E\vee C\ne F\right)$$