A short sequel to EWD 863
In EWD863, I left at the end the derivation of de Morgan's Laws as an exercise to the reader. The following proof, however, is too beautiful to remain unrecorded. I recall —with numbers as in EWD863— the axioms 

[ P ∧ Q ≡ P ≡ Q ≡ P ∨ Q ] 
(9)

[ P ∨ ¬Q ≡ P ∨ Q ≡ P ]  (14) 
and the theorems  
[ ¬¬Q ≡ Q ]  (19) 
[¬(P ≡ Q) ≡ ¬P ≡ Q ] .  (20) 
From (14), we derive with P := ¬P and P,Q := Q,P respectively:  
[ ¬P ∨ ¬Q ≡ ¬P ∨ Q ≡ ¬P ]  
[ Q ∨ ¬P ≡ Q ∨ P ≡ Q ] ;  
from those two with Leibniz's Principle (and symmetry of v and ≡ )  
[ ¬P ∨ ¬Q ≡ ¬P ≡ Q ≡ P ∨ Q ] ;  
from that one with  (20) 
[ ¬P ∨ ¬Q ≡ ¬( P ≡ Q ≡ P ∨ Q ) ] ,  
and finally with (9)  
[ ¬P ∨ ¬Q ≡ ¬( P ∧ Q ) ] .  (25) 
With (19) —and [¬P ≡ ¬P], which is a syntactic descendant  
[ ¬P ∧ ¬Q ≡ ¬( P ∨ Q ) ]  (26) 
follows readily from (25). 