Theorem sb2imi

Distribute substitution over implication. Compare al2imi. (Contributed by Steven Nguyen, 13-Aug-2023.)

Hypothesis
sb2imi.1
\( \vdash \varphi \rightarrow \psi \rightarrow \chi \)
Conclusion
\( \vdash [ t' / x ] \, \varphi \rightarrow [ t' / x ] \, \psi \rightarrow [ t' / x ] \, \chi \)
Proof
sb2imi.1
l1
sbimi _
\( \vdash [ t' / x ] \, \varphi \rightarrow [ t' / x ] \, (\psi \rightarrow \chi) \)
sbi1
\( \vdash [ t' / x ] \, (\psi \rightarrow \chi) \rightarrow [ t' / x ] \, \psi \rightarrow [ t' / x ] \, \chi \)
syl l1 _