Derived inference rule
= 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.