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 e. CH /\ B e. HAtoms ) -> ( A C. ( A vH B ) <-> A

Proof

Step Hyp Ref Expression
1 atelch 
 |-  ( B e. HAtoms -> B e. CH )
2 chnle 
 |-  ( ( A e. CH /\ B e. CH ) -> ( -. B C_ A <-> A C. ( A vH B ) ) )
3 1 2 sylan2 
 |-  ( ( A e. CH /\ B e. HAtoms ) -> ( -. B C_ A <-> A C. ( A vH B ) ) )
4 chcv1 
 |-  ( ( A e. CH /\ B e. HAtoms ) -> ( -. B C_ A <-> A
5 3 4 bitr3d 
 |-  ( ( A e. CH /\ B e. HAtoms ) -> ( A C. ( A vH B ) <-> A