Theorem otthne

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

	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 3	otth	⊢ ( ⟨ 𝐴 , 𝐵 , 𝐶 ⟩ = ⟨ 𝐷 , 𝐸 , 𝐹 ⟩ ↔ ( 𝐴 = 𝐷 ∧ 𝐵 = 𝐸 ∧ 𝐶 = 𝐹 ) )
5	4	notbii	⊢ ( ¬ ⟨ 𝐴 , 𝐵 , 𝐶 ⟩ = ⟨ 𝐷 , 𝐸 , 𝐹 ⟩ ↔ ¬ ( 𝐴 = 𝐷 ∧ 𝐵 = 𝐸 ∧ 𝐶 = 𝐹 ) )
6		3ianor	⊢ ( ¬ ( 𝐴 = 𝐷 ∧ 𝐵 = 𝐸 ∧ 𝐶 = 𝐹 ) ↔ ( ¬ 𝐴 = 𝐷 ∨ ¬ 𝐵 = 𝐸 ∨ ¬ 𝐶 = 𝐹 ) )
7	5 6	bitri	⊢ ( ¬ ⟨ 𝐴 , 𝐵 , 𝐶 ⟩ = ⟨ 𝐷 , 𝐸 , 𝐹 ⟩ ↔ ( ¬ 𝐴 = 𝐷 ∨ ¬ 𝐵 = 𝐸 ∨ ¬ 𝐶 = 𝐹 ) )
8		df-ne	⊢ ( ⟨ 𝐴 , 𝐵 , 𝐶 ⟩ ≠ ⟨ 𝐷 , 𝐸 , 𝐹 ⟩ ↔ ¬ ⟨ 𝐴 , 𝐵 , 𝐶 ⟩ = ⟨ 𝐷 , 𝐸 , 𝐹 ⟩ )
9		df-ne	⊢ ( 𝐴 ≠ 𝐷 ↔ ¬ 𝐴 = 𝐷 )
10		df-ne	⊢ ( 𝐵 ≠ 𝐸 ↔ ¬ 𝐵 = 𝐸 )
11		df-ne	⊢ ( 𝐶 ≠ 𝐹 ↔ ¬ 𝐶 = 𝐹 )
12	9 10 11	3orbi123i	⊢ ( ( 𝐴 ≠ 𝐷 ∨ 𝐵 ≠ 𝐸 ∨ 𝐶 ≠ 𝐹 ) ↔ ( ¬ 𝐴 = 𝐷 ∨ ¬ 𝐵 = 𝐸 ∨ ¬ 𝐶 = 𝐹 ) )
13	7 8 12	3bitr4i	⊢ ( ⟨ 𝐴 , 𝐵 , 𝐶 ⟩ ≠ ⟨ 𝐷 , 𝐸 , 𝐹 ⟩ ↔ ( 𝐴 ≠ 𝐷 ∨ 𝐵 ≠ 𝐸 ∨ 𝐶 ≠ 𝐹 ) )