Metamath Proof Explorer


Theorem chdmm3

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

Ref Expression
Assertion chdmm3 A C B C A B = A B

Proof

Step Hyp Ref Expression
1 choccl B C B C
2 chdmm1 A C B C A B = A B
3 1 2 sylan2 A C B C A B = A B
4 ococ B C B = B
5 4 adantl A C B C B = B
6 5 oveq2d A C B C A B = A B
7 3 6 eqtrd A C B C A B = A B