Theorem spsbim

Distribute substitution over implication. Closed form of sbimi. Specialization of implication. (Contributed by NM, 5-Aug-1993.) (Proof shortened by Andrew Salmon, 25-May-2011.) Revise [df-sb]. (Revised by BJ, 22-Dec-2020.) (Proof shortened by Steven Nguyen, 24-Jul-2023.)

Conclusion
\( \vdash \forall x \, (\varphi \rightarrow \psi) \rightarrow [ t' / x ] \, \varphi \rightarrow [ t' / x ] \, \psi \)
Proof
l0
stdpc4
\( \vdash \forall x \, (\varphi \rightarrow \psi) \rightarrow [ t' / x ] \, (\varphi \rightarrow \psi) \)
sbi1
\( \vdash [ t' / x ] \, (\varphi \rightarrow \psi) \rightarrow [ t' / x ] \, \varphi \rightarrow [ t' / x ] \, \psi \)
syl l0 _