Conservativity of intuitionistic propositional logic over its implicational fragment
= Conservativity of intuitionistic propositional logic over its implicational fragment
If $\Gamma$ and $\varphi$ are implicational and $\Gamma\vdash_{\mathrm{IPC}}\varphi$, then $\Gamma\vdash_{\mathrm{IPC}(\to)}\varphi$. Soundness for Kripke semantics followed by <Kripke completeness of implicational intuitionistic logic> proves the claim.