Goal: (Kφ↔¬K¬Kφ)
System: S5(m)
using derived rules: true
1. S5(m) ⊢ (¬Kφ→K¬Kφ)	(A5)
2. S5(m) ⊢ (¬K¬Kφ→¬¬Kφ)	(CP:1)
3. S5(m) ⊢ (¬¬Kφ↔Kφ)	(A1)
4. S5(m) ⊢ (¬K¬Kφ→Kφ)	(SUB:3,2)
5. S5(m) ⊢ (K¬Kφ→¬Kφ)	(A3)
6. S5(m) ⊢ (¬¬Kφ→¬K¬Kφ)	(CP:5)
7. S5(m) ⊢ (Kφ→¬K¬Kφ)	(SUB:3,6)
8. S5(m) ⊢ (Kφ↔¬K¬Kφ)	(EI:4,7)