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