Goal: (Ki¬φ→¬Kiφ)
System: S5(m)
using derived rules: true
1. S5(m) ⊢ (Ki¬φ→¬φ)	(A3)
2. S5(m) ⊢ (Kiφ→φ)	(A3)
3. S5(m) ⊢ (¬φ→¬Kiφ)	(CP:2)
4. S5(m) ⊢ (Ki¬φ→¬Kiφ)	(HS:1,3)