Metamath Proof Explorer


Theorem chlub

Description: Hilbert lattice join is the least upper bound of two elements. (Contributed by NM, 12-Jun-2004) (New usage is discouraged.)

Ref Expression
Assertion chlub ACBCCCACBCABC

Proof

Step Hyp Ref Expression
1 chsh ACAS
2 chsh BCBS
3 shlub ASBSCCACBCABC
4 2 3 syl3an2 ASBCCCACBCABC
5 1 4 syl3an1 ACBCCCACBCABC