Theorem ledii

Description: An ortholattice is distributive in one ordering direction. (Contributed by NM, 6-Aug-2004) (New usage is discouraged.)

	Ref	Expression
Hypotheses	ledi.1	|- A e. CH
	ledi.2	|- B e. CH
	ledi.3	|- C e. CH
Assertion	ledii	|- ( ( A i^i B ) vH ( A i^i C ) ) C_ ( A 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		inss1	|- ( A i^i B ) C_ A
5		inss1	|- ( A i^i C ) C_ A
6	1 2	chincli	|- ( A i^i B ) e. CH
7	1 3	chincli	|- ( A i^i C ) e. CH
8	6 7 1	chlubii	|- ( ( ( A i^i B ) C_ A /\ ( A i^i C ) C_ A ) -> ( ( A i^i B ) vH ( A i^i C ) ) C_ A )
9	4 5 8	mp2an	|- ( ( A i^i B ) vH ( A i^i C ) ) C_ A
10		inss2	|- ( A i^i B ) C_ B
11		inss2	|- ( A i^i C ) C_ C
12	6 2 7 3	chlej12i	|- ( ( ( A i^i B ) C_ B /\ ( A i^i C ) C_ C ) -> ( ( A i^i B ) vH ( A i^i C ) ) C_ ( B vH C ) )
13	10 11 12	mp2an	|- ( ( A i^i B ) vH ( A i^i C ) ) C_ ( B vH C )
14	9 13	ssini	|- ( ( A i^i B ) vH ( A i^i C ) ) C_ ( A i^i ( B vH C ) )