Definition
Disjunction Elimination Inference Rule (Propositional Hilbert Calculus)
In the propositional Hilbert calculus, proof by cases is the derived elimination inference rule for disjunction. For any theory
and formulas : Here
abbreviates : if each case yields , the disjunction suffices to derive .