Theorem otthne

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

	Ref	Expression
Hypotheses	otthne.1	⊢ 𝐴 ∈ V
	otthne.2	⊢ 𝐵 ∈ V
	otthne.3	⊢ 𝐶 ∈ V
Assertion	otthne	⊢ ( ⟨ ⟨ 𝐴 , 𝐵 ⟩ , 𝐶 ⟩ ≠ ⟨ ⟨ 𝐷 , 𝐸 ⟩ , 𝐹 ⟩ ↔ ( 𝐴 ≠ 𝐷 ∨ 𝐵 ≠ 𝐸 ∨ 𝐶 ≠ 𝐹 ) )

Proof

Step	Hyp	Ref	Expression
1		otthne.1	⊢ 𝐴 ∈ V
2		otthne.2	⊢ 𝐵 ∈ V
3		otthne.3	⊢ 𝐶 ∈ V
4	1 2	opthne	⊢ ( ⟨ 𝐴 , 𝐵 ⟩ ≠ ⟨ 𝐷 , 𝐸 ⟩ ↔ ( 𝐴 ≠ 𝐷 ∨ 𝐵 ≠ 𝐸 ) )
5	4	orbi1i	⊢ ( ( ⟨ 𝐴 , 𝐵 ⟩ ≠ ⟨ 𝐷 , 𝐸 ⟩ ∨ 𝐶 ≠ 𝐹 ) ↔ ( ( 𝐴 ≠ 𝐷 ∨ 𝐵 ≠ 𝐸 ) ∨ 𝐶 ≠ 𝐹 ) )
6		opex	⊢ ⟨ 𝐴 , 𝐵 ⟩ ∈ V
7	6 3	opthne	⊢ ( ⟨ ⟨ 𝐴 , 𝐵 ⟩ , 𝐶 ⟩ ≠ ⟨ ⟨ 𝐷 , 𝐸 ⟩ , 𝐹 ⟩ ↔ ( ⟨ 𝐴 , 𝐵 ⟩ ≠ ⟨ 𝐷 , 𝐸 ⟩ ∨ 𝐶 ≠ 𝐹 ) )
8		df-3or	⊢ ( ( 𝐴 ≠ 𝐷 ∨ 𝐵 ≠ 𝐸 ∨ 𝐶 ≠ 𝐹 ) ↔ ( ( 𝐴 ≠ 𝐷 ∨ 𝐵 ≠ 𝐸 ) ∨ 𝐶 ≠ 𝐹 ) )
9	5 7 8	3bitr4i	⊢ ( ⟨ ⟨ 𝐴 , 𝐵 ⟩ , 𝐶 ⟩ ≠ ⟨ ⟨ 𝐷 , 𝐸 ⟩ , 𝐹 ⟩ ↔ ( 𝐴 ≠ 𝐷 ∨ 𝐵 ≠ 𝐸 ∨ 𝐶 ≠ 𝐹 ) )