Theorem sbrimvw

Substitution in an implication with a variable not free in the antecedent affects only the consequent. Version of sbrim based on fewer axioms, but with more disjoint variable conditions. (Contributed by Wolf Lammen, 29-Jan-2024.) Remove DV condition. (Revised by Wolf Lammen, 5-Jun-2026.)

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