Goal: (Kφ→Kψ)
System: K(m)
using derived rules: false
1. K(m) ⊢ (φ→ψ)	(premise)
2. K(m) ⊢ K(φ→ψ)	(R2:1)
3. K(m) ⊢ ((Kφ∧K(φ→ψ))→Kψ)	(A2)
4. K(m) ⊢ (((Kφ∧K(φ→ψ))→Kψ)→(K(φ→ψ)→(Kφ→Kψ)))	(A1)
5. K(m) ⊢ (K(φ→ψ)→(Kφ→Kψ))	(R1:3,4)
6. K(m) ⊢ (Kφ→Kψ)	(R1:2,5)