Proposition 86: Negation elimination for entailment (inference rule)

Given that the negation \neg \psi entails \neg \phi , we may infer \phi entails \psi : \cfrac{\neg \psi \vdash \neg \phi}{\phi \vdash \psi}.

Proof: By [69], we infer the double negation \neg \neg \phi entails \neg \neg \psi . Thus, we may infer using [85] that \phi entails \psi . \square