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

Metamath Proof Explorer

Theorem otth2

Description: Ordered triple theorem, with triple expressed with ordered pairs. (Contributed by NM, 1-May-1995) (Revised by Mario Carneiro, 26-Apr-2015)

Ref Expression
Hypotheses otth.1 
|- A e. _V
otth.2 
|- B e. _V
otth.3 
|- R e. _V
Assertion otth2 
|- ( <. <. A , B >. , R >. = <. <. C , D >. , S >. <-> ( A = C /\ B = D /\ R = S ) )

Proof

Step Hyp Ref Expression
1 otth.1 
 |-  A e. _V
2 otth.2 
 |-  B e. _V
3 otth.3 
 |-  R e. _V
4 1 2 opth 
 |-  ( <. A , B >. = <. C , D >. <-> ( A = C /\ B = D ) )
5 4 anbi1i 
 |-  ( ( <. A , B >. = <. C , D >. /\ R = S ) <-> ( ( A = C /\ B = D ) /\ R = S ) )
6 opex 
 |-  <. A , B >. e. _V
7 6 3 opth 
 |-  ( <. <. A , B >. , R >. = <. <. C , D >. , S >. <-> ( <. A , B >. = <. C , D >. /\ R = S ) )
8 df-3an 
 |-  ( ( A = C /\ B = D /\ R = S ) <-> ( ( A = C /\ B = D ) /\ R = S ) )
9 5 7 8 3bitr4i 
 |-  ( <. <. A , B >. , R >. = <. <. C , D >. , S >. <-> ( A = C /\ B = D /\ R = S ) )