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 𝐴C
chj12.2 𝐵C
chj12.3 𝐶C
Assertion chj12i ( 𝐴 ( 𝐵 𝐶 ) ) = ( 𝐵 ( 𝐴 𝐶 ) )

Proof

Step Hyp Ref Expression
1 chj12.1 𝐴C
2 chj12.2 𝐵C
3 chj12.3 𝐶C
4 1 2 chjcomi ( 𝐴 𝐵 ) = ( 𝐵 𝐴 )
5 4 oveq1i ( ( 𝐴 𝐵 ) ∨ 𝐶 ) = ( ( 𝐵 𝐴 ) ∨ 𝐶 )
6 1 2 3 chjassi ( ( 𝐴 𝐵 ) ∨ 𝐶 ) = ( 𝐴 ( 𝐵 𝐶 ) )
7 2 1 3 chjassi ( ( 𝐵 𝐴 ) ∨ 𝐶 ) = ( 𝐵 ( 𝐴 𝐶 ) )
8 5 6 7 3eqtr3i ( 𝐴 ( 𝐵 𝐶 ) ) = ( 𝐵 ( 𝐴 𝐶 ) )