Theorem 63: Conditional introduction (inference rule)

Given that \phi entails \psi , we may infer that the implication (\phi \Rightarrow \psi) holds: \cfrac{\phi \vdash \psi}{\vdash (\phi \Rightarrow \psi)}.

Proof: Assume the conjunction \phi \wedge \neg \psi , where \neg \psi is the negation of \psi . Using conjunction elimination, we infer \neg \psi holds. By weakening, we infer (under the assumption \phi \wedge \neg \psi ) that \phi entails \neg \psi . But we have as the premise that \phi entails \psi , so by negation introduction we infer (still with the assumption \phi \wedge \neg \psi remaining in place) that \neg \phi holds. Thus, \phi \wedge \neg \psi entails \neg \phi .

Assume \phi \wedge \neg \psi again. By conjunction elimination, we may infer that \phi holds. Thus, \phi \wedge \neg \psi also entails \phi ; by negation introduction, we therefore infer that \neg (\phi \wedge \neg \psi) holds. But \phi \Rightarrow \psi is short for just this. \square