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

Metamath Proof Explorer

Theorem cmm1i

Description: A Hilbert lattice element commutes with its meet. (Contributed by NM, 7-Aug-2004) (New usage is discouraged.)

Step	Hyp	Ref	Expression
1		pjoml2.1	$⊢ A \in C_{ℋ}$
2		pjoml2.2	$⊢ B \in C_{ℋ}$
3	1 2	chincli	$⊢ A \cap B \in C_{ℋ}$
4		inss1	$⊢ A \cap B \subseteq A$
5	3 1 4	lecmii	$⊢ (A \cap B) 𝐶_{ℋ} A$
6	3 1 5	cmcmii	$⊢ A 𝐶_{ℋ} (A \cap B)$