is a natural deduction proof system for classical propositional logic. It is identical to NJp except that it replaces the rule with the rule: