Metamath Proof Explorer


Theorem chjidm

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

Ref Expression
Assertion chjidm A C A A = A

Proof

Step Hyp Ref Expression
1 inidm A A = A
2 1 oveq2i A A A = A A
3 chabs1 A C A C A A A = A
4 3 anidms A C A A A = A
5 2 4 eqtr3id A C A A = A