Metamath Proof Explorer
Description: Hilbert lattice absorption law. From definition of lattice in
Kalmbach p. 14. (Contributed by NM, 16-Jun-2004)
(New usage is discouraged.)
|
|
Ref |
Expression |
|
Hypotheses |
chabs.1 |
⊢ 𝐴 ∈ Cℋ |
|
|
chabs.2 |
⊢ 𝐵 ∈ Cℋ |
|
Assertion |
chabs2i |
⊢ ( 𝐴 ∩ ( 𝐴 ∨ℋ 𝐵 ) ) = 𝐴 |
Proof
Step |
Hyp |
Ref |
Expression |
1 |
|
chabs.1 |
⊢ 𝐴 ∈ Cℋ |
2 |
|
chabs.2 |
⊢ 𝐵 ∈ Cℋ |
3 |
|
chabs2 |
⊢ ( ( 𝐴 ∈ Cℋ ∧ 𝐵 ∈ Cℋ ) → ( 𝐴 ∩ ( 𝐴 ∨ℋ 𝐵 ) ) = 𝐴 ) |
4 |
1 2 3
|
mp2an |
⊢ ( 𝐴 ∩ ( 𝐴 ∨ℋ 𝐵 ) ) = 𝐴 |