Metamath Proof Explorer

Theorem otthg

Description: Ordered triple theorem, closed form. (Contributed by Alexander van der Vekens, 10-Mar-2018)

Ref Expression
Assertion otthg 
|- ( ( A e. U /\ B e. V /\ C e. W ) -> ( <. A , B , C >. = <. D , E , F >. <-> ( A = D /\ B = E /\ C = F ) ) )

Proof

Step Hyp Ref Expression
1 df-ot 
 |-  <. A , B , C >. = <. <. A , B >. , C >.
2 df-ot 
 |-  <. D , E , F >. = <. <. D , E >. , F >.
3 1 2 eqeq12i 
 |-  ( <. A , B , C >. = <. D , E , F >. <-> <. <. A , B >. , C >. = <. <. D , E >. , F >. )
4 opex 
 |-  <. A , B >. e. _V
5 opthg 
 |-  ( ( <. A , B >. e. _V /\ C e. W ) -> ( <. <. A , B >. , C >. = <. <. D , E >. , F >. <-> ( <. A , B >. = <. D , E >. /\ C = F ) ) )
6 4 5 mpan 
 |-  ( C e. W -> ( <. <. A , B >. , C >. = <. <. D , E >. , F >. <-> ( <. A , B >. = <. D , E >. /\ C = F ) ) )
7 opthg 
 |-  ( ( A e. U /\ B e. V ) -> ( <. A , B >. = <. D , E >. <-> ( A = D /\ B = E ) ) )
8 7 anbi1d 
 |-  ( ( A e. U /\ B e. V ) -> ( ( <. A , B >. = <. D , E >. /\ C = F ) <-> ( ( A = D /\ B = E ) /\ C = F ) ) )
9 df-3an 
 |-  ( ( A = D /\ B = E /\ C = F ) <-> ( ( A = D /\ B = E ) /\ C = F ) )
10 8 9 bitr4di 
 |-  ( ( A e. U /\ B e. V ) -> ( ( <. A , B >. = <. D , E >. /\ C = F ) <-> ( A = D /\ B = E /\ C = F ) ) )
11 6 10 sylan9bbr 
 |-  ( ( ( A e. U /\ B e. V ) /\ C e. W ) -> ( <. <. A , B >. , C >. = <. <. D , E >. , F >. <-> ( A = D /\ B = E /\ C = F ) ) )
12 11 3impa 
 |-  ( ( A e. U /\ B e. V /\ C e. W ) -> ( <. <. A , B >. , C >. = <. <. D , E >. , F >. <-> ( A = D /\ B = E /\ C = F ) ) )
13 3 12 bitrid 
 |-  ( ( A e. U /\ B e. V /\ C e. W ) -> ( <. A , B , C >. = <. D , E , F >. <-> ( A = D /\ B = E /\ C = F ) ) )