Metamath Proof Explorer


Theorem chm1i

Description: Meet with lattice one in CH . (Contributed by NM, 24-Oct-1999) (New usage is discouraged.)

Ref Expression
Hypothesis ch0le.1 𝐴C
Assertion chm1i ( 𝐴 ∩ ℋ ) = 𝐴

Proof

Step Hyp Ref Expression
1 ch0le.1 𝐴C
2 1 chssii 𝐴 ⊆ ℋ
3 df-ss ( 𝐴 ⊆ ℋ ↔ ( 𝐴 ∩ ℋ ) = 𝐴 )
4 2 3 mpbi ( 𝐴 ∩ ℋ ) = 𝐴