Metamath Proof Explorer


Theorem chjjdiri

Description: Hilbert lattice join distributes over itself. (Contributed by NM, 29-Apr-2006) (New usage is discouraged.)

Ref Expression
Hypotheses chj12.1
|- A e. CH
chj12.2
|- B e. CH
chj12.3
|- C e. CH
Assertion chjjdiri
|- ( ( A vH B ) vH C ) = ( ( A vH C ) vH ( B vH C ) )

Proof

Step Hyp Ref Expression
1 chj12.1
 |-  A e. CH
2 chj12.2
 |-  B e. CH
3 chj12.3
 |-  C e. CH
4 3 chjidmi
 |-  ( C vH C ) = C
5 4 oveq2i
 |-  ( ( A vH B ) vH ( C vH C ) ) = ( ( A vH B ) vH C )
6 1 2 3 3 chj4i
 |-  ( ( A vH B ) vH ( C vH C ) ) = ( ( A vH C ) vH ( B vH C ) )
7 5 6 eqtr3i
 |-  ( ( A vH B ) vH C ) = ( ( A vH C ) vH ( B vH C ) )