Metamath Proof Explorer


Theorem chm0i

Description: Meet with Hilbert lattice zero. (Contributed by NM, 6-Aug-2004) (New usage is discouraged.)

Ref Expression
Hypothesis ch0le.1 A C
Assertion chm0i A 0 = 0

Proof

Step Hyp Ref Expression
1 ch0le.1 A C
2 inss2 A 0 0
3 1 ch0lei 0 A
4 ssid 0 0
5 3 4 ssini 0 A 0
6 2 5 eqssi A 0 = 0