Metamath Proof Explorer

Theorem chj12

Description: A rearrangement of Hilbert lattice join. (Contributed by NM, 15-Jun-2006) (New usage is discouraged.)

Ref Expression
Assertion chj12 ⊢A∈Cℋ∧B∈Cℋ∧C∈Cℋ→A∨ℋB∨ℋC=B∨ℋA∨ℋC

Proof

Step Hyp Ref Expression
1 chjcom ⊢A∈Cℋ∧B∈Cℋ→A∨ℋB=B∨ℋA
2 1 3adant3 ⊢A∈Cℋ∧B∈Cℋ∧C∈Cℋ→A∨ℋB=B∨ℋA
3 2 oveq1d ⊢A∈Cℋ∧B∈Cℋ∧C∈Cℋ→A∨ℋB∨ℋC=B∨ℋA∨ℋC
4 chjass ⊢A∈Cℋ∧B∈Cℋ∧C∈Cℋ→A∨ℋB∨ℋC=A∨ℋB∨ℋC
5 chjass ⊢B∈Cℋ∧A∈Cℋ∧C∈Cℋ→B∨ℋA∨ℋC=B∨ℋA∨ℋC
6 5 3com12 ⊢A∈Cℋ∧B∈Cℋ∧C∈Cℋ→B∨ℋA∨ℋC=B∨ℋA∨ℋC
7 3 4 6 3eqtr3d ⊢A∈Cℋ∧B∈Cℋ∧C∈Cℋ→A∨ℋB∨ℋC=B∨ℋA∨ℋC