 TAUT combined with modus ponens (MP) gives us the full inferential power of PC. \(\OB\)-K, which is the K-axiom common to all normal modal logics, tells us that if a material conditional is obligatory, and its antecedent is too, then so is its  consequent.[18]  NC tells us that \(p\) is obligatory only if its negation isn’t. The rule \(\OB\)-NEC tells us that if anything is a theorem, then the claim that that thing is obligatory is also a theorem. Note that this guarantees that something is always obligatory (even if only logical  truths).[19]