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