Theorem sbimi

Distribute substitution over implication. (Contributed by NM, 25-Jun-1998.) Revise [df-sb]. (Revised by BJ, 22-Dec-2020.) (Proof shortened by Steven Nguyen, 24-Jul-2023.)

Hypothesis
sbimi.1
\( \vdash \varphi \rightarrow \psi \)
Conclusion
\( \vdash [ t' / x ] \, \varphi \rightarrow [ t' / x ] \, \psi \)
Proof
sbimi.1
l1
sbt _
\( \vdash [ t' / x ] \, (\varphi \rightarrow \psi) \)
sbi1
\( \vdash [ t' / x ] \, (\varphi \rightarrow \psi) \rightarrow [ t' / x ] \, \varphi \rightarrow [ t' / x ] \, \psi \)
ax-mp l1 _