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