Metamath Proof Explorer


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