Theorem lediri

Description: An ortholattice is distributive in one ordering direction. (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	lediri	|- ( ( A i^i C ) vH ( B i^i C ) ) C_ ( ( A vH B ) i^i 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	ledii	|- ( ( C i^i A ) vH ( C i^i B ) ) C_ ( C i^i ( A vH B ) )
5		incom	|- ( A i^i C ) = ( C i^i A )
6		incom	|- ( B i^i C ) = ( C i^i B )
7	5 6	oveq12i	|- ( ( A i^i C ) vH ( B i^i C ) ) = ( ( C i^i A ) vH ( C i^i B ) )
8		incom	|- ( ( A vH B ) i^i C ) = ( C i^i ( A vH B ) )
9	4 7 8	3sstr4i	|- ( ( A i^i C ) vH ( B i^i C ) ) C_ ( ( A vH B ) i^i C )