Theorem sblim

Substitution in an implication with a variable not free in the consequent affects only the antecedent. (Contributed by NM, 14-Nov-2013.) (Revised by Mario Carneiro, 4-Oct-2016.)

Hypothesis
sblim.1
\( \vdash \Finv x \, \psi \)
Conclusion
\( \vdash [ y' / x ] \, (\varphi \rightarrow \psi) \leftrightarrow [ y' / x ] \, \varphi \rightarrow \psi \)
Proof
l0
sbim
\( \vdash [ y' / x ] \, (\varphi \rightarrow \psi) \leftrightarrow [ y' / x ] \, \varphi \rightarrow [ y' / x ] \, \psi \)
sblim.1
sbf _
imbi2i _
\( \vdash [ y' / x ] \, \varphi \rightarrow [ y' / x ] \, \psi \leftrightarrow [ y' / x ] \, \varphi \rightarrow \psi \)
bitri l0 _