chj4i

Description: Rearrangement of the join of 4 Hilbert lattice elements. (Contributed by NM, 29-Apr-2006) (New usage is discouraged.)

	Ref	Expression
Hypotheses	chj12.1	$⊢ A \in C_{ℋ}$
	chj12.2	$⊢ B \in C_{ℋ}$
	chj12.3	$⊢ C \in C_{ℋ}$
	chj4.4	$⊢ D \in C_{ℋ}$
Assertion	chj4i	$⊢ (A \lor_{ℋ} B) \lor_{ℋ} (C \lor_{ℋ} D) = (A \lor_{ℋ} C) \lor_{ℋ} (B \lor_{ℋ} D)$

Step	Hyp	Ref	Expression
1		chj12.1	$⊢ A \in C_{ℋ}$
2		chj12.2	$⊢ B \in C_{ℋ}$
3		chj12.3	$⊢ C \in C_{ℋ}$
4		chj4.4	$⊢ D \in C_{ℋ}$
5	2 3 4	chj12i	$⊢ B \lor_{ℋ} (C \lor_{ℋ} D) = C \lor_{ℋ} (B \lor_{ℋ} D)$
6	5	oveq2i	$⊢ A \lor_{ℋ} (B \lor_{ℋ} (C \lor_{ℋ} D)) = A \lor_{ℋ} (C \lor_{ℋ} (B \lor_{ℋ} D))$
7	3 4	chjcli	$⊢ C \lor_{ℋ} D \in C_{ℋ}$
8	1 2 7	chjassi	$⊢ (A \lor_{ℋ} B) \lor_{ℋ} (C \lor_{ℋ} D) = A \lor_{ℋ} (B \lor_{ℋ} (C \lor_{ℋ} D))$
9	2 4	chjcli	$⊢ B \lor_{ℋ} D \in C_{ℋ}$
10	1 3 9	chjassi	$⊢ (A \lor_{ℋ} C) \lor_{ℋ} (B \lor_{ℋ} D) = A \lor_{ℋ} (C \lor_{ℋ} (B \lor_{ℋ} D))$
11	6 8 10	3eqtr4i	$⊢ (A \lor_{ℋ} B) \lor_{ℋ} (C \lor_{ℋ} D) = (A \lor_{ℋ} C) \lor_{ℋ} (B \lor_{ℋ} D)$

Metamath Proof Explorer