Metamath Proof Explorer


Theorem chdmm4i

Description: De Morgan's law for meet in a Hilbert lattice. (Contributed by NM, 21-Jun-2004) (New usage is discouraged.)

Ref Expression
Hypotheses ch0le.1 A C
chjcl.2 B C
Assertion chdmm4i A B = A B

Proof

Step Hyp Ref Expression
1 ch0le.1 A C
2 chjcl.2 B C
3 2 choccli B C
4 1 3 chdmm2i A B = A B
5 2 pjococi B = B
6 5 oveq2i A B = A B
7 4 6 eqtri A B = A B