Theorem nf5-1

One direction of nf5 can be proved with a smaller footprint on axiom usage. (Contributed by Wolf Lammen, 16-Sep-2021.)

Conclusion
\( \vdash \forall x \, (\varphi \rightarrow \forall x \, \varphi) \rightarrow \Finv x \, \varphi \)
Proof
l0
exim
\( \vdash \forall x \, (\varphi \rightarrow \forall x \, \varphi) \rightarrow \exists x \, \varphi \rightarrow \exists x \, \forall x \, \varphi \)
hbe1a
\( \vdash \exists x \, \forall x \, \varphi \rightarrow \forall x \, \varphi \)
syl6 l0 _
nfd _