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 ⊢ A ∈ V
otthne.2 ⊢ B ∈ V
otthne.3 ⊢ C ∈ V
Assertion otthne ⊢ A B C ≠ D E F ↔ A ≠ D ∨ B ≠ E ∨ C ≠ F

Proof

Step Hyp Ref Expression
1 otthne.1 ⊢ A ∈ V
2 otthne.2 ⊢ B ∈ V
3 otthne.3 ⊢ C ∈ V
4 1 2 3 otth ⊢ A B C = D E F ↔ A = D ∧ B = E ∧ C = F
5 4 notbii ⊢ ¬ A B C = D E F ↔ ¬ A = D ∧ B = E ∧ C = F
6 3ianor ⊢ ¬ A = D ∧ B = E ∧ C = F ↔ ¬ A = D ∨ ¬ B = E ∨ ¬ C = F
7 5 6 bitri ⊢ ¬ A B C = D E F ↔ ¬ A = D ∨ ¬ B = E ∨ ¬ C = F
8 df-ne ⊢ A B C ≠ D E F ↔ ¬ A B C = D E F
9 df-ne ⊢ A ≠ D ↔ ¬ A = D
10 df-ne ⊢ B ≠ E ↔ ¬ B = E
11 df-ne ⊢ C ≠ F ↔ ¬ C = F
12 9 10 11 3orbi123i ⊢ A ≠ D ∨ B ≠ E ∨ C ≠ F ↔ ¬ A = D ∨ ¬ B = E ∨ ¬ C = F
13 7 8 12 3bitr4i ⊢ A B C ≠ D E F ↔ A ≠ D ∨ B ≠ E ∨ C ≠ F