Metamath Proof Explorer


Theorem chdmj3i

Description: De Morgan's law for join 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 chdmj3i 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 chdmj1i A B = A B
5 2 pjococi B = B
6 5 ineq2i A B = A B
7 4 6 eqtri A B = A B