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	|- A e. CH
	chj12.2	|- B e. CH
	chj12.3	|- C e. CH
	chj4.4	|- D e. CH
Assertion	chj4i	|- ( ( A vH B ) vH ( C vH D ) ) = ( ( A vH C ) vH ( B vH D ) )

Proof

Step	Hyp	Ref	Expression
1		chj12.1	|- A e. CH
2		chj12.2	|- B e. CH
3		chj12.3	|- C e. CH
4		chj4.4	|- D e. CH
5	2 3 4	chj12i	|- ( B vH ( C vH D ) ) = ( C vH ( B vH D ) )
6	5	oveq2i	|- ( A vH ( B vH ( C vH D ) ) ) = ( A vH ( C vH ( B vH D ) ) )
7	3 4	chjcli	|- ( C vH D ) e. CH
8	1 2 7	chjassi	|- ( ( A vH B ) vH ( C vH D ) ) = ( A vH ( B vH ( C vH D ) ) )
9	2 4	chjcli	|- ( B vH D ) e. CH
10	1 3 9	chjassi	|- ( ( A vH C ) vH ( B vH D ) ) = ( A vH ( C vH ( B vH D ) ) )
11	6 8 10	3eqtr4i	|- ( ( A vH B ) vH ( C vH D ) ) = ( ( A vH C ) vH ( B vH D ) )