Theorem otthne

Description: Contrapositive of the ordered triple theorem. (Contributed by Scott Fenton, 21-Aug-2024)

	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	opthne	$$⊢⟨A,B⟩\ne ⟨D,E⟩\leftrightarrow \left(A\ne D\vee B\ne E\right)$$
5	4	orbi1i	$$⊢\left(⟨A,B⟩\ne ⟨D,E⟩\vee C\ne F\right)\leftrightarrow \left(\left(A\ne D\vee B\ne E\right)\vee C\ne F\right)$$
6		opex	$$⊢⟨A,B⟩\in \mathrm{V}$$
7	6 3	opthne	$$⊢⟨⟨A,B⟩,C⟩\ne ⟨⟨D,E⟩,F⟩\leftrightarrow \left(⟨A,B⟩\ne ⟨D,E⟩\vee C\ne F\right)$$
8		df-3or	$$⊢\left(A\ne D\vee B\ne E\vee C\ne F\right)\leftrightarrow \left(\left(A\ne D\vee B\ne E\right)\vee C\ne F\right)$$
9	5 7 8	3bitr4i	$$⊢⟨⟨A,B⟩,C⟩\ne ⟨⟨D,E⟩,F⟩\leftrightarrow \left(A\ne D\vee B\ne E\vee C\ne F\right)$$