Inference rule

An inference rule licenses a conclusion from specified premises, possibly with side conditions. A derived inference rule is justified by a logical derivation using the primitive inference rules; using it subsequently abbreviates that logical derivation.

A derived inference rule abbreviates a logical derivation from the primitive inference rules. Its use retains the assumptions and side conditions required by that logical derivation; proving the abbreviation once allows subsequent proofs to use the rule without expanding every intermediate line.