Theorem nfntht

Closed form of nfnth. (Contributed by BJ, 16-Sep-2021.) (Proof shortened by Wolf Lammen, 4-Sep-2022.)

Conclusion

\( \vdash \neg \exists x \, \varphi \rightarrow \Finv x \, \varphi \)

Proof

pm2.21

nfd _