 Along with the ∧ rules reformulated in the above sequent-to-sequent style, and the structural rule (Id)—(Weakening) and (Cut) being derivable—these rules render provable exactly those sequents in {∧,∨,→}-fragment of intuitionistic logic, while for the corresponding fragment of classical logic, one would need to add a further principle governing implication, such as the following subcontrariety rule: