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	⊢ 𝐴 ∈ V
	otth.2	⊢ 𝐵 ∈ V
	otth.3	⊢ 𝑅 ∈ V
Assertion	otth2	⊢ ( ⟨ ⟨ 𝐴 , 𝐵 ⟩ , 𝑅 ⟩ = ⟨ ⟨ 𝐶 , 𝐷 ⟩ , 𝑆 ⟩ ↔ ( 𝐴 = 𝐶 ∧ 𝐵 = 𝐷 ∧ 𝑅 = 𝑆 ) )

Proof

Step	Hyp	Ref	Expression
1		otth.1	⊢ 𝐴 ∈ V
2		otth.2	⊢ 𝐵 ∈ V
3		otth.3	⊢ 𝑅 ∈ V
4	1 2	opth	⊢ ( ⟨ 𝐴 , 𝐵 ⟩ = ⟨ 𝐶 , 𝐷 ⟩ ↔ ( 𝐴 = 𝐶 ∧ 𝐵 = 𝐷 ) )
5	4	anbi1i	⊢ ( ( ⟨ 𝐴 , 𝐵 ⟩ = ⟨ 𝐶 , 𝐷 ⟩ ∧ 𝑅 = 𝑆 ) ↔ ( ( 𝐴 = 𝐶 ∧ 𝐵 = 𝐷 ) ∧ 𝑅 = 𝑆 ) )
6		opex	⊢ ⟨ 𝐴 , 𝐵 ⟩ ∈ V
7	6 3	opth	⊢ ( ⟨ ⟨ 𝐴 , 𝐵 ⟩ , 𝑅 ⟩ = ⟨ ⟨ 𝐶 , 𝐷 ⟩ , 𝑆 ⟩ ↔ ( ⟨ 𝐴 , 𝐵 ⟩ = ⟨ 𝐶 , 𝐷 ⟩ ∧ 𝑅 = 𝑆 ) )
8		df-3an	⊢ ( ( 𝐴 = 𝐶 ∧ 𝐵 = 𝐷 ∧ 𝑅 = 𝑆 ) ↔ ( ( 𝐴 = 𝐶 ∧ 𝐵 = 𝐷 ) ∧ 𝑅 = 𝑆 ) )
9	5 7 8	3bitr4i	⊢ ( ⟨ ⟨ 𝐴 , 𝐵 ⟩ , 𝑅 ⟩ = ⟨ ⟨ 𝐶 , 𝐷 ⟩ , 𝑆 ⟩ ↔ ( 𝐴 = 𝐶 ∧ 𝐵 = 𝐷 ∧ 𝑅 = 𝑆 ) )