Elimination rules are rules that are used to derive subformulae of compound formulae already in the derivation. The connective or operator specified in the name of the rule is the main connective or operator of one of the formulae to which the rule is applied.
Elimination rules can only be applied forwards in the CPL.
For information on a particular elimination rule, please select that rule from the Elimination Rules menu under the Rules tab of the navigation panel.