Theorem nftht

Closed form of nfth. (Contributed by Wolf Lammen, 19-Aug-2018.) (Proof shortened by BJ, 16-Sep-2021.) (Proof shortened by Wolf Lammen, 3-Sep-2022.)

Conclusion
\( \vdash \forall x \, \varphi \rightarrow \Finv x \, \varphi \)
Proof
ax-1
nfd _