Metamath Proof Explorer


Theorem chdmm2i

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 AC
chjcl.2 BC
Assertion chdmm2i AB=AB

Proof

Step Hyp Ref Expression
1 ch0le.1 AC
2 chjcl.2 BC
3 1 choccli AC
4 3 2 chdmm1i AB=AB
5 1 pjococi A=A
6 5 oveq1i AB=AB
7 4 6 eqtri AB=AB