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

Metamath Proof Explorer

Theorem chjjdiri

Description: Hilbert lattice join distributes over itself. (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_{ℋ}$
Assertion	chjjdiri	$⊢ (A \lor_{ℋ} B) \lor_{ℋ} C = (A \lor_{ℋ} C) \lor_{ℋ} (B \lor_{ℋ} C)$

Step	Hyp	Ref	Expression
1		chj12.1	$⊢ A \in C_{ℋ}$
2		chj12.2	$⊢ B \in C_{ℋ}$
3		chj12.3	$⊢ C \in C_{ℋ}$
4	3	chjidmi	$⊢ C \lor_{ℋ} C = C$
5	4	oveq2i	$⊢ (A \lor_{ℋ} B) \lor_{ℋ} (C \lor_{ℋ} C) = (A \lor_{ℋ} B) \lor_{ℋ} C$
6	1 2 3 3	chj4i	$⊢ (A \lor_{ℋ} B) \lor_{ℋ} (C \lor_{ℋ} C) = (A \lor_{ℋ} C) \lor_{ℋ} (B \lor_{ℋ} C)$
7	5 6	eqtr3i	$⊢ (A \lor_{ℋ} B) \lor_{ℋ} C = (A \lor_{ℋ} C) \lor_{ℋ} (B \lor_{ℋ} C)$