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