Theorem chj4i

Description: Rearrangement of the join of 4 Hilbert lattice elements. (Contributed by NM, 29-Apr-2006) (New usage is discouraged.)

	Ref	Expression
Hypotheses	chj12.1	⊢ 𝐴 ∈ Cℋ
	chj12.2	⊢ 𝐵 ∈ Cℋ
	chj12.3	⊢ 𝐶 ∈ Cℋ
	chj4.4	⊢ 𝐷 ∈ Cℋ
Assertion	chj4i	⊢ ( ( 𝐴 ∨ℋ 𝐵 ) ∨ℋ ( 𝐶 ∨ℋ 𝐷 ) ) = ( ( 𝐴 ∨ℋ 𝐶 ) ∨ℋ ( 𝐵 ∨ℋ 𝐷 ) )

Proof

Step	Hyp	Ref	Expression
1		chj12.1	⊢ 𝐴 ∈ Cℋ
2		chj12.2	⊢ 𝐵 ∈ Cℋ
3		chj12.3	⊢ 𝐶 ∈ Cℋ
4		chj4.4	⊢ 𝐷 ∈ Cℋ
5	2 3 4	chj12i	⊢ ( 𝐵 ∨ℋ ( 𝐶 ∨ℋ 𝐷 ) ) = ( 𝐶 ∨ℋ ( 𝐵 ∨ℋ 𝐷 ) )
6	5	oveq2i	⊢ ( 𝐴 ∨ℋ ( 𝐵 ∨ℋ ( 𝐶 ∨ℋ 𝐷 ) ) ) = ( 𝐴 ∨ℋ ( 𝐶 ∨ℋ ( 𝐵 ∨ℋ 𝐷 ) ) )
7	3 4	chjcli	⊢ ( 𝐶 ∨ℋ 𝐷 ) ∈ Cℋ
8	1 2 7	chjassi	⊢ ( ( 𝐴 ∨ℋ 𝐵 ) ∨ℋ ( 𝐶 ∨ℋ 𝐷 ) ) = ( 𝐴 ∨ℋ ( 𝐵 ∨ℋ ( 𝐶 ∨ℋ 𝐷 ) ) )
9	2 4	chjcli	⊢ ( 𝐵 ∨ℋ 𝐷 ) ∈ Cℋ
10	1 3 9	chjassi	⊢ ( ( 𝐴 ∨ℋ 𝐶 ) ∨ℋ ( 𝐵 ∨ℋ 𝐷 ) ) = ( 𝐴 ∨ℋ ( 𝐶 ∨ℋ ( 𝐵 ∨ℋ 𝐷 ) ) )
11	6 8 10	3eqtr4i	⊢ ( ( 𝐴 ∨ℋ 𝐵 ) ∨ℋ ( 𝐶 ∨ℋ 𝐷 ) ) = ( ( 𝐴 ∨ℋ 𝐶 ) ∨ℋ ( 𝐵 ∨ℋ 𝐷 ) )