 Normal modal distribution axiom

The normal distribution axiom says that a boxed implication and its boxed antecedent give the boxed consequent. Together with the necessitation rule, it permits boxed versions of propositional deductions. Under an arithmetic interpretation it is the internal modus-ponens condition among the Hilbert-Bernays-Löb derivability conditions. It does not permit dropping a box to assert the enclosed sentence.