Goal: (K¬K¬φ↔¬K¬φ)
System: S5(m)
using derived rules: true
1. S5(m) ⊢ (K¬K¬φ→¬K¬φ)	(A3)
2. S5(m) ⊢ (¬K¬φ→K¬K¬φ)	(A5)
3. S5(m) ⊢ (K¬K¬φ↔¬K¬φ)	(EI:2,1)