Theorem chjidmi

Description: Idempotent law for Hilbert lattice join. (Contributed by NM, 15-Jun-2004) (New usage is discouraged.)

	Ref	Expression
Hypothesis	chjidm.1	|- A e. CH
Assertion	chjidmi	|- ( A vH A ) = A

Proof

Step	Hyp	Ref	Expression
1		chjidm.1	|- A e. CH
2		chjidm	|- ( A e. CH -> ( A vH A ) = A )
3	1 2	ax-mp	|- ( A vH A ) = A