Theorem hbnt

Closed theorem version of bound-variable hypothesis builder hbn. (Contributed by NM, 10-May-1993.) (Proof shortened by Wolf Lammen, 14-Oct-2021.)

Conclusion

\( \vdash \forall x \, (\varphi \rightarrow \forall x \, \varphi) \rightarrow \neg \varphi \rightarrow \forall x \, \neg \varphi \)

Proof

nf5-1

nfnd _

nf5rd _