 Implication distribution rule

From $\varphi \to (\psi \to \rho )$ infer $(\varphi \to \psi )\to (\varphi \to \rho )$. Assume $\varphi \to \psi$, then assume $\varphi$. Implication elimination rule gives $\psi$ and $\psi \to \rho$, hence $\rho$. Discharge $\varphi$ and then $\varphi \to \psi$ by the implication introduction rule. The original premise and any surrounding assumptions remain available.