Theorem 47: The weakening rule (inference rule)

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

Proof: Assume \phi . By conjunction introduction, we infer that the conjunction \phi \wedge \psi holds. Then, using conjunction elimination, we infer \psi holds. Thus, we have showed \phi entails \psi . \square