Metamath Proof Explorer


Theorem otthne

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

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 opthne A B D E A D B E
5 4 orbi1i A B D E C F A D B E C F
6 opex A B V
7 6 3 opthne A B C D E F A B D E C F
8 df-3or A D B E C F A D B E C F
9 5 7 8 3bitr4i A B C D E F A D B E C F