Rule. subj_intro_iii
(H ∧ A ∧ B ∧ C ⊢ D) → (H ⊢ A → B → C → D)