 As concerns axiomatics, a Hilbert calculus for \({{\cal L}}\) is obtained by joining up the (schema) axioms of both systems. Thus, \({{\cal L}}\) has, among others, two \(K\) axioms, two necessitation rules and just one Modus Ponens (because implication \(\to\) is shared). Considering that the language of \({{\cal L}}\) has mixed formulas (as \(\varphi\) above), schema variables occurring in the schema rules of the given logics can now be replaced in \({{\cal L}}\) by mixed formulas. For instance, \(\varphi\) can be derived in \({{\cal L}}\) from the formula \((\square_2 p \to p)\) by an application of the necessitation rule for the box \(\square_1\).