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 |
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 |