Theorem hbn

If \( x \) is not free in \( \varphi \), it is not free in \( \neg \varphi \). (Contributed by NM, 10-Jan-1993.) (Proof shortened by Wolf Lammen, 17-Dec-2017.)

Hypothesis
hbn.1
\( \vdash \varphi \rightarrow \forall x \, \varphi \)
Conclusion
\( \vdash \neg \varphi \rightarrow \forall x \, \neg \varphi \)
Proof
l0
hbnt
\( \vdash \forall x \, (\varphi \rightarrow \forall x \, \varphi) \rightarrow \neg \varphi \rightarrow \forall x \, \neg \varphi \)
hbn.1
\( \vdash \varphi \rightarrow \forall x \, \varphi \)
mpg l0 _