Implication creation rule
= Implication creation rule
{title2=$\psi\vdash\phi\to\psi$}
From a <logical derivation> of $\psi$, infer $\phi\to\psi$ under the same surrounding assumptions. To derive the rule, temporarily assume $\phi$, retain the available $\psi$, and discharge $\phi$ by the <implication introduction rule>. Its being unused is allowed.