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 e. _V
otthne.2 
|- B e. _V
otthne.3 
|- C e. _V
Assertion otthne 
|- ( <. A , B , C >. =/= <. D , E , F >. <-> ( A =/= D \/ B =/= E \/ C =/= F ) )

Proof

Step Hyp Ref Expression
1 otthne.1 
 |-  A e. _V
2 otthne.2 
 |-  B e. _V
3 otthne.3 
 |-  C e. _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 ) )