Goal: (Kφ↔KKφ)
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)
9. S5(m) ⊢ (KKφ↔K¬K¬Kφ)	(KD↔:8)
10. S5(m) ⊢ (¬K¬Kφ→K¬K¬Kφ)	(A5)
11. S5(m) ⊢ (K¬K¬Kφ→¬K¬Kφ)	(A3)
12. S5(m) ⊢ (K¬K¬Kφ↔¬K¬Kφ)	(EI:10,11)
13. S5(m) ⊢ (KKφ↔¬K¬Kφ)	(HS↔:9,12)
14. S5(m) ⊢ ((KKφ↔¬K¬Kφ)→(¬K¬Kφ↔KKφ))	(A1)
15. S5(m) ⊢ (¬K¬Kφ↔KKφ)	(R1:13,14)
16. S5(m) ⊢ (Kφ↔KKφ)	(HS↔:8,15)