Theorem sbi2

Introduction of implication into substitution. (Contributed by NM, 14-May-1993.)

Conclusion
\( \vdash ([ y' / x ] \, \varphi \rightarrow [ y' / x ] \, \psi) \rightarrow [ y' / x ] \, (\varphi \rightarrow \psi) \)
Proof
l0
sbn
\( \vdash [ y' / x ] \, (\neg \varphi) \leftrightarrow \neg [ y' / x ] \, \varphi \)
pm2.21
sbimi _
\( \vdash [ y' / x ] \, (\neg \varphi) \rightarrow [ y' / x ] \, (\varphi \rightarrow \psi) \)
l3
sylbir l0 _
ax-1
sbimi _
ja l3 _