Metamath Proof Explorer
Description: Hilbert lattice absorption law. From definition of lattice in
Kalmbach p. 14. (Contributed by NM, 10Jun2004)
(New usage is discouraged.)


Ref 
Expression 

Hypotheses 
chabs.1 
⊢ 𝐴 ∈ C_{ℋ} 


chabs.2 
⊢ 𝐵 ∈ C_{ℋ} 

Assertion 
chabs1i 
⊢ ( 𝐴 ∨_{ℋ} ( 𝐴 ∩ 𝐵 ) ) = 𝐴 
Proof
Step 
Hyp 
Ref 
Expression 
1 

chabs.1 
⊢ 𝐴 ∈ C_{ℋ} 
2 

chabs.2 
⊢ 𝐵 ∈ C_{ℋ} 
3 

chabs1 
⊢ ( ( 𝐴 ∈ C_{ℋ} ∧ 𝐵 ∈ C_{ℋ} ) → ( 𝐴 ∨_{ℋ} ( 𝐴 ∩ 𝐵 ) ) = 𝐴 ) 
4 
1 2 3

mp2an 
⊢ ( 𝐴 ∨_{ℋ} ( 𝐴 ∩ 𝐵 ) ) = 𝐴 