otthg

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

		Ref	Expression
	Assertion	otthg	$⊢ (A \in U \land B \in V \land C \in W) \to (⟨A, B, C⟩ = ⟨D, E, F⟩ \leftrightarrow (A = D \land B = E \land C = F))$

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⟩ \leftrightarrow ⟨⟨A, B⟩, C⟩ = ⟨⟨D, E⟩, F⟩$
4		opex	$⊢ ⟨A, B⟩ \in V$
5		opthg	$⊢ (⟨A, B⟩ \in V \land C \in W) \to (⟨⟨A, B⟩, C⟩ = ⟨⟨D, E⟩, F⟩ \leftrightarrow (⟨A, B⟩ = ⟨D, E⟩ \land C = F))$
6	4 5	mpan	$⊢ C \in W \to (⟨⟨A, B⟩, C⟩ = ⟨⟨D, E⟩, F⟩ \leftrightarrow (⟨A, B⟩ = ⟨D, E⟩ \land C = F))$
7		opthg	$⊢ (A \in U \land B \in V) \to (⟨A, B⟩ = ⟨D, E⟩ \leftrightarrow (A = D \land B = E))$
8	7	anbi1d	$⊢ (A \in U \land B \in V) \to ((⟨A, B⟩ = ⟨D, E⟩ \land C = F) \leftrightarrow ((A = D \land B = E) \land C = F))$
9		df-3an	$⊢ (A = D \land B = E \land C = F) \leftrightarrow ((A = D \land B = E) \land C = F)$
10	8 9	bitr4di	$⊢ (A \in U \land B \in V) \to ((⟨A, B⟩ = ⟨D, E⟩ \land C = F) \leftrightarrow (A = D \land B = E \land C = F))$
11	6 10	sylan9bbr	$⊢ ((A \in U \land B \in V) \land C \in W) \to (⟨⟨A, B⟩, C⟩ = ⟨⟨D, E⟩, F⟩ \leftrightarrow (A = D \land B = E \land C = F))$
12	11	3impa	$⊢ (A \in U \land B \in V \land C \in W) \to (⟨⟨A, B⟩, C⟩ = ⟨⟨D, E⟩, F⟩ \leftrightarrow (A = D \land B = E \land C = F))$
13	3 12	bitrid	$⊢ (A \in U \land B \in V \land C \in W) \to (⟨A, B, C⟩ = ⟨D, E, F⟩ \leftrightarrow (A = D \land B = E \land C = F))$

Metamath Proof Explorer