Linear Depth Deduction with Subformula Property for Intuitionistic Epistemic Logic