Derived inference rule

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.