Then $\mathrm{\Gamma },\psi {⊢}_{\text{IPC}}\phi$. Moreover, if $p$ is a primitive proposition and $\psi$ is any proposition, then

$$\mathrm{\Gamma }[p:=\psi ]{⊢}_{\text{IPC}}\phi [p:=\psi ].$$