Theorem chjjdiri

Description: Hilbert lattice join distributes over itself. (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
Assertion	chjjdiri	|- ( ( A vH B ) vH C ) = ( ( A vH C ) vH ( B vH C ) )

Proof

Step	Hyp	Ref	Expression
1		chj12.1	|- A e. CH
2		chj12.2	|- B e. CH
3		chj12.3	|- C e. CH
4	3	chjidmi	|- ( C vH C ) = C
5	4	oveq2i	|- ( ( A vH B ) vH ( C vH C ) ) = ( ( A vH B ) vH C )
6	1 2 3 3	chj4i	|- ( ( A vH B ) vH ( C vH C ) ) = ( ( A vH C ) vH ( B vH C ) )
7	5 6	eqtr3i	|- ( ( A vH B ) vH C ) = ( ( A vH C ) vH ( B vH C ) )