Theorem
sbh
Substitution for a variable not free in a wff does not affect it. (Contributed by NM, 14-May-1993.)
Hypothesis
sbh.1
\( \vdash \varphi \rightarrow \forall x \, \varphi \)
Conclusion
\( \vdash [ y' / x ] \, \varphi \leftrightarrow \varphi \)
Proof
sbh.1
nf5i
_
sbf
_
This is the content in the right pane.