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

Metamath Proof Explorer

Theorem chabs1i

Description: Hilbert lattice absorption law. From definition of lattice in Kalmbach p. 14. (Contributed by NM, 10-Jun-2004) (New usage is discouraged.)

	Ref	Expression
Hypotheses	chabs.1	$⊢ A \in C_{ℋ}$
	chabs.2	$⊢ B \in C_{ℋ}$
Assertion	chabs1i	$⊢ A \lor_{ℋ} (A \cap B) = A$

Proof

Step	Hyp	Ref	Expression
1		chabs.1	$⊢ A \in C_{ℋ}$
2		chabs.2	$⊢ B \in C_{ℋ}$
3		chabs1	$⊢ (A \in C_{ℋ} \land B \in C_{ℋ}) \to A \lor_{ℋ} (A \cap B) = A$
4	1 2 3	mp2an	$⊢ A \lor_{ℋ} (A \cap B) = A$