chj12

Description: A rearrangement of Hilbert lattice join. (Contributed by NM, 15-Jun-2006) (New usage is discouraged.)

		Ref	Expression
	Assertion	chj12	$⊢ (A \in C_{ℋ} \land B \in C_{ℋ} \land C \in C_{ℋ}) \to A \lor_{ℋ} (B \lor_{ℋ} C) = B \lor_{ℋ} (A \lor_{ℋ} C)$

Step	Hyp	Ref	Expression
1		chjcom	$⊢ (A \in C_{ℋ} \land B \in C_{ℋ}) \to A \lor_{ℋ} B = B \lor_{ℋ} A$
2	1	3adant3	$⊢ (A \in C_{ℋ} \land B \in C_{ℋ} \land C \in C_{ℋ}) \to A \lor_{ℋ} B = B \lor_{ℋ} A$
3	2	oveq1d	$⊢ (A \in C_{ℋ} \land B \in C_{ℋ} \land C \in C_{ℋ}) \to (A \lor_{ℋ} B) \lor_{ℋ} C = (B \lor_{ℋ} A) \lor_{ℋ} C$
4		chjass	$⊢ (A \in C_{ℋ} \land B \in C_{ℋ} \land C \in C_{ℋ}) \to (A \lor_{ℋ} B) \lor_{ℋ} C = A \lor_{ℋ} (B \lor_{ℋ} C)$
5		chjass	$⊢ (B \in C_{ℋ} \land A \in C_{ℋ} \land C \in C_{ℋ}) \to (B \lor_{ℋ} A) \lor_{ℋ} C = B \lor_{ℋ} (A \lor_{ℋ} C)$
6	5	3com12	$⊢ (A \in C_{ℋ} \land B \in C_{ℋ} \land C \in C_{ℋ}) \to (B \lor_{ℋ} A) \lor_{ℋ} C = B \lor_{ℋ} (A \lor_{ℋ} C)$
7	3 4 6	3eqtr3d	$⊢ (A \in C_{ℋ} \land B \in C_{ℋ} \land C \in C_{ℋ}) \to A \lor_{ℋ} (B \lor_{ℋ} C) = B \lor_{ℋ} (A \lor_{ℋ} C)$

Metamath Proof Explorer