A rule of inference that governs when one may remove a connective $\circ$ from a formula, e.g., conjunction elimination,

Some formulae have only an introduction rule and no corresponding elimination rule. For example, the propositional constant verum ($\top$) has the introduction rule:

but no elimination rule.