Metamath Proof Explorer

Theorem chlej1

Description: Add join to both sides of Hilbert lattice ordering. (Contributed by NM, 22-Jun-2004) (New usage is discouraged.)

Ref Expression
Assertion chlej1 
|- ( ( ( A e. CH /\ B e. CH /\ C e. CH ) /\ A C_ B ) -> ( A vH C ) C_ ( B vH C ) )

Proof

Step Hyp Ref Expression
1 chsh 
 |-  ( A e. CH -> A e. SH )
2 chsh 
 |-  ( B e. CH -> B e. SH )
3 chsh 
 |-  ( C e. CH -> C e. SH )
4 shlej1 
 |-  ( ( ( A e. SH /\ B e. SH /\ C e. SH ) /\ A C_ B ) -> ( A vH C ) C_ ( B vH C ) )
5 1 2 3 4 syl3anl 
 |-  ( ( ( A e. CH /\ B e. CH /\ C e. CH ) /\ A C_ B ) -> ( A vH C ) C_ ( B vH C ) )