Implication distribution rule
= Implication distribution rule
{title2=$\phi\to(\psi\to\rho)\vdash(\phi\to\psi)\to(\phi\to\rho)$}
From $\phi\to(\psi\to\rho)$ infer $(\phi\to\psi)\to(\phi\to\rho)$. Assume $\phi\to\psi$, then assume $\phi$. <Implication elimination rule> gives $\psi$ and $\psi\to\rho$, hence $\rho$. Discharge $\phi$ and then $\phi\to\psi$ by the <implication introduction rule>. The original premise and any surrounding assumptions remain available.