Theorem pjoml5i

Description: The orthomodular law. Remark in Kalmbach p. 22. (Contributed by NM, 12-Jun-2006) (New usage is discouraged.)

	Ref	Expression
Hypotheses	pjoml2.1	|- A e. CH
	pjoml2.2	|- B e. CH
Assertion	pjoml5i	|- ( A vH ( ( _|_ ` A ) i^i ( A vH B ) ) ) = ( A vH B )

Proof

Step	Hyp	Ref	Expression
1		pjoml2.1	|- A e. CH
2		pjoml2.2	|- B e. CH
3	1 2	chub1i	|- A C_ ( A vH B )
4	1 2	chjcli	|- ( A vH B ) e. CH
5	1 4	pjoml2i	|- ( A C_ ( A vH B ) -> ( A vH ( ( _|_ ` A ) i^i ( A vH B ) ) ) = ( A vH B ) )
6	3 5	ax-mp	|- ( A vH ( ( _|_ ` A ) i^i ( A vH B ) ) ) = ( A vH B )