Definition
Derived Inference Rule
A derived inference rule is an inference rule whose instances can be derived from their premises using the primitive rules of a calculus:
Each application abbreviates a derivation from its premises; it does not add a primitive rule to the calculus.
Example
Two applications of modus ponens
In a Hilbert calculus with modus ponens, the rule
abbreviates two applications: derive
from and , then derive from and .