In this paper we propose proof systems without labels for the intuitionistic modal logic
that are based on a new multi-contextual sequent structure appropriate to deal with such a logic. We first give a label-free natural deduction system and thus derive natural deduction systems for the classical modal logic
and also for an intermediate logic
. Then we define a label-free sequent calculus for
and prove its soundness and completeness. The study of this calculus leads to a decision procedure for
and thus to an alternative syntactic proof of its decidability.