subj_elim

Rule. subj_elim
(H1 ⊢ A → B) → (H2 ⊢ A) → (H1 ∧ H2 ⊢ B)

Subjunction elimination, a modus ponens that operates with sequents rather than plain propositions.