 The essential breakthrough of Gentzen’s treatment was to characterize each logical operator in isolation, with rules of its own, rules in which only that operator would explicitly feature. Moreover, the rules in question would deal only with a single occurrence (in dominant position) of the operator in question. The rule for reasoning to a conclusion with the operator dominant was called the operator’s introduction rule; while the rule for reasoning from a premise with the operator dominant was called its elimination rule. 