Theorem
sbim
Implication inside and outside of a substitution are equivalent. (Contributed by NM, 14-May-1993.)
Conclusion
\( \vdash [ y' / x ] \, (\varphi \rightarrow \psi) \leftrightarrow [ y' / x ] \, \varphi \rightarrow [ y' / x ] \, \psi \)
Proof
l0
sbi1
sbi2
impbii
l0
_
This is the content in the right pane.