Implication creation rule ($\psi ⊢\varphi \to \psi$)

From a logical derivation of $\psi$, infer $\varphi \to \psi$ under the same surrounding assumptions. To derive the rule, temporarily assume $\varphi$, retain the available $\psi$, and discharge $\varphi$ by the implication introduction rule. Its being unused is allowed.