This approach to studying the minimal intuitionistic modal logic is based on a generalization of Gentzen's original sequent calculus introduced and developed by the author in a previous paper [see Ann. Pure Appl. Logic 58 (1992), no. 3, 229--246; MR1191942 (93k:03056)]. The complete proof-theoretic treatment of the calculus is presented, including the cut elimination theorem with some of its consequences. The author considers the corresponding 2-natural deduction system, followed by the normalization theorem, and analyzes its relationship with the 2-sequent calculus. Such an approach to the proof-theoretic analysis of logical systems seems to be very natural, fruitful and applicable to a wide class of logics.