Metamath Proof Explorer


Theorem chcv2

Description: The Hilbert lattice has the covering property. (Contributed by NM, 11-Jun-2004) (New usage is discouraged.)

Ref Expression
Assertion chcv2 A C B HAtoms A A B A A B

Proof

Step Hyp Ref Expression
1 atelch B HAtoms B C
2 chnle A C B C ¬ B A A A B
3 1 2 sylan2 A C B HAtoms ¬ B A A A B
4 chcv1 A C B HAtoms ¬ B A A A B
5 3 4 bitr3d A C B HAtoms A A B A A B