 (Equivalently, in view of Weakening, one could give a formulation with “Δ” as a set-variable for the right sequent premiss, and carry both “Γ” and “Δ” down to the conclusion-sequent, as in the formulation of (→E) above.) In the terminology of Dummett (1991) all of the rules we have seen are pure (their schematic formulation involves mention only of a single connective) and simple (each formulation mentions it only once), this last rule is also oblique: a discharged assumption has the connective in question as its main connective. One can trade in this obliqueness for a loss of simplicity, changing the →-elimination rule from the familiar Modus Ponens principle above to a version incorporating Peirce’s Law (“(p → q) → p ≻ p”), due to  Kanger:[5]