Definition
Implication Elimination Inference Rule (Propositional Hilbert Calculus)
In the propositional Hilbert calculus, implication has the following elimination inference rule, for arbitrary formulas
: This is the derivability form of modus ponens, which is already the calculus’s primitive inference rule.