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 ) )