Metamath Proof Explorer


Theorem chj12i

Description: A rearrangement of Hilbert lattice join. (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 chj12i
|- ( A vH ( B vH C ) ) = ( B vH ( A 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 1 2 chjcomi
 |-  ( A vH B ) = ( B vH A )
5 4 oveq1i
 |-  ( ( A vH B ) vH C ) = ( ( B vH A ) vH C )
6 1 2 3 chjassi
 |-  ( ( A vH B ) vH C ) = ( A vH ( B vH C ) )
7 2 1 3 chjassi
 |-  ( ( B vH A ) vH C ) = ( B vH ( A vH C ) )
8 5 6 7 3eqtr3i
 |-  ( A vH ( B vH C ) ) = ( B vH ( A vH C ) )