This is an inofficial mirror of http://metamath.tirix.org for personal testing of a visualizer extension only.

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 ∈ C ℋ
chj12.2 ⊢ B ∈ C ℋ
chj12.3 ⊢ C ∈ C ℋ
Assertion chj12i ⊢ A ∨ ℋ B ∨ ℋ C = B ∨ ℋ A ∨ ℋ C

Proof

Step Hyp Ref Expression
1 chj12.1 ⊢ A ∈ C ℋ
2 chj12.2 ⊢ B ∈ C ℋ
3 chj12.3 ⊢ C ∈ C ℋ
4 1 2 chjcomi ⊢ A ∨ ℋ B = B ∨ ℋ A
5 4 oveq1i ⊢ A ∨ ℋ B ∨ ℋ C = B ∨ ℋ A ∨ ℋ C
6 1 2 3 chjassi ⊢ A ∨ ℋ B ∨ ℋ C = A ∨ ℋ B ∨ ℋ C
7 2 1 3 chjassi ⊢ B ∨ ℋ A ∨ ℋ C = B ∨ ℋ A ∨ ℋ C
8 5 6 7 3eqtr3i ⊢ A ∨ ℋ B ∨ ℋ C = B ∨ ℋ A ∨ ℋ C