Metamath Proof Explorer


Theorem chdmj2i

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 chdmj2i A B = A B

Proof

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