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

Metamath Proof Explorer

Theorem otthg

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

		Ref	Expression
	Assertion	otthg	⊢ ( ( 𝐴 ∈ 𝑈 ∧ 𝐵 ∈ 𝑉 ∧ 𝐶 ∈ 𝑊 ) → ( ⟨ 𝐴 , 𝐵 , 𝐶 ⟩ = ⟨ 𝐷 , 𝐸 , 𝐹 ⟩ ↔ ( 𝐴 = 𝐷 ∧ 𝐵 = 𝐸 ∧ 𝐶 = 𝐹 ) ) )

Proof

Step	Hyp	Ref	Expression
1		df-ot	⊢ ⟨ 𝐴 , 𝐵 , 𝐶 ⟩ = ⟨ ⟨ 𝐴 , 𝐵 ⟩ , 𝐶 ⟩
2		df-ot	⊢ ⟨ 𝐷 , 𝐸 , 𝐹 ⟩ = ⟨ ⟨ 𝐷 , 𝐸 ⟩ , 𝐹 ⟩
3	1 2	eqeq12i	⊢ ( ⟨ 𝐴 , 𝐵 , 𝐶 ⟩ = ⟨ 𝐷 , 𝐸 , 𝐹 ⟩ ↔ ⟨ ⟨ 𝐴 , 𝐵 ⟩ , 𝐶 ⟩ = ⟨ ⟨ 𝐷 , 𝐸 ⟩ , 𝐹 ⟩ )
4		opex	⊢ ⟨ 𝐴 , 𝐵 ⟩ ∈ V
5		opthg	⊢ ( ( ⟨ 𝐴 , 𝐵 ⟩ ∈ V ∧ 𝐶 ∈ 𝑊 ) → ( ⟨ ⟨ 𝐴 , 𝐵 ⟩ , 𝐶 ⟩ = ⟨ ⟨ 𝐷 , 𝐸 ⟩ , 𝐹 ⟩ ↔ ( ⟨ 𝐴 , 𝐵 ⟩ = ⟨ 𝐷 , 𝐸 ⟩ ∧ 𝐶 = 𝐹 ) ) )
6	4 5	mpan	⊢ ( 𝐶 ∈ 𝑊 → ( ⟨ ⟨ 𝐴 , 𝐵 ⟩ , 𝐶 ⟩ = ⟨ ⟨ 𝐷 , 𝐸 ⟩ , 𝐹 ⟩ ↔ ( ⟨ 𝐴 , 𝐵 ⟩ = ⟨ 𝐷 , 𝐸 ⟩ ∧ 𝐶 = 𝐹 ) ) )
7		opthg	⊢ ( ( 𝐴 ∈ 𝑈 ∧ 𝐵 ∈ 𝑉 ) → ( ⟨ 𝐴 , 𝐵 ⟩ = ⟨ 𝐷 , 𝐸 ⟩ ↔ ( 𝐴 = 𝐷 ∧ 𝐵 = 𝐸 ) ) )
8	7	anbi1d	⊢ ( ( 𝐴 ∈ 𝑈 ∧ 𝐵 ∈ 𝑉 ) → ( ( ⟨ 𝐴 , 𝐵 ⟩ = ⟨ 𝐷 , 𝐸 ⟩ ∧ 𝐶 = 𝐹 ) ↔ ( ( 𝐴 = 𝐷 ∧ 𝐵 = 𝐸 ) ∧ 𝐶 = 𝐹 ) ) )
9		df-3an	⊢ ( ( 𝐴 = 𝐷 ∧ 𝐵 = 𝐸 ∧ 𝐶 = 𝐹 ) ↔ ( ( 𝐴 = 𝐷 ∧ 𝐵 = 𝐸 ) ∧ 𝐶 = 𝐹 ) )
10	8 9	bitr4di	⊢ ( ( 𝐴 ∈ 𝑈 ∧ 𝐵 ∈ 𝑉 ) → ( ( ⟨ 𝐴 , 𝐵 ⟩ = ⟨ 𝐷 , 𝐸 ⟩ ∧ 𝐶 = 𝐹 ) ↔ ( 𝐴 = 𝐷 ∧ 𝐵 = 𝐸 ∧ 𝐶 = 𝐹 ) ) )
11	6 10	sylan9bbr	⊢ ( ( ( 𝐴 ∈ 𝑈 ∧ 𝐵 ∈ 𝑉 ) ∧ 𝐶 ∈ 𝑊 ) → ( ⟨ ⟨ 𝐴 , 𝐵 ⟩ , 𝐶 ⟩ = ⟨ ⟨ 𝐷 , 𝐸 ⟩ , 𝐹 ⟩ ↔ ( 𝐴 = 𝐷 ∧ 𝐵 = 𝐸 ∧ 𝐶 = 𝐹 ) ) )
12	11	3impa	⊢ ( ( 𝐴 ∈ 𝑈 ∧ 𝐵 ∈ 𝑉 ∧ 𝐶 ∈ 𝑊 ) → ( ⟨ ⟨ 𝐴 , 𝐵 ⟩ , 𝐶 ⟩ = ⟨ ⟨ 𝐷 , 𝐸 ⟩ , 𝐹 ⟩ ↔ ( 𝐴 = 𝐷 ∧ 𝐵 = 𝐸 ∧ 𝐶 = 𝐹 ) ) )
13	3 12	bitrid	⊢ ( ( 𝐴 ∈ 𝑈 ∧ 𝐵 ∈ 𝑉 ∧ 𝐶 ∈ 𝑊 ) → ( ⟨ 𝐴 , 𝐵 , 𝐶 ⟩ = ⟨ 𝐷 , 𝐸 , 𝐹 ⟩ ↔ ( 𝐴 = 𝐷 ∧ 𝐵 = 𝐸 ∧ 𝐶 = 𝐹 ) ) )