This is an inofficial mirror of http://metamath.tirix.org for personal testing of a visualizer extension only.

Metamath Proof Explorer

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 ⊢ ( ⟨ 𝐴 , 𝐵 , 𝐶 ⟩ ≠ ⟨ 𝐷 , 𝐸 , 𝐹 ⟩ ↔ ( 𝐴 ≠ 𝐷 ∨ 𝐵 ≠ 𝐸 ∨ 𝐶 ≠ 𝐹 ) )