Theorem lejdiri

Description: An ortholattice is distributive in one ordering direction (join version). (Contributed by NM, 27-Apr-2006) (New usage is discouraged.)

	Ref	Expression
Hypotheses	ledi.1	|- A e. CH
	ledi.2	|- B e. CH
	ledi.3	|- C e. CH
Assertion	lejdiri	|- ( ( A i^i B ) vH C ) C_ ( ( A vH C ) i^i ( B vH C ) )

Proof

Step	Hyp	Ref	Expression
1		ledi.1	|- A e. CH
2		ledi.2	|- B e. CH
3		ledi.3	|- C e. CH
4	3 1 2	lejdii	|- ( C vH ( A i^i B ) ) C_ ( ( C vH A ) i^i ( C vH B ) )
5	1 2	chincli	|- ( A i^i B ) e. CH
6	5 3	chjcomi	|- ( ( A i^i B ) vH C ) = ( C vH ( A i^i B ) )
7	1 3	chjcomi	|- ( A vH C ) = ( C vH A )
8	2 3	chjcomi	|- ( B vH C ) = ( C vH B )
9	7 8	ineq12i	|- ( ( A vH C ) i^i ( B vH C ) ) = ( ( C vH A ) i^i ( C vH B ) )
10	4 6 9	3sstr4i	|- ( ( A i^i B ) vH C ) C_ ( ( A vH C ) i^i ( B vH C ) )