This paper is a continuation of Inoué [5]. As already mentioned in the paper, a number of intuitionistic provable formulas are given with a Hilbert-style proof. For that, we make use of a family of intuitionistic deduction theorems, which are also presented in this paper by means of Mizar system [2], [1]. Our axiom system of intuitionistic propositional logic IPC is based on the propositional subsystem of H1-