Theorem nfd

Deduce that \( x \) is not free in \( \psi \) in a context. (Contributed by Wolf Lammen, 16-Sep-2021.)

Hypothesis
nfd.1
\( \vdash \varphi \rightarrow \exists x \, \psi \rightarrow \forall x \, \psi \)
Conclusion
\( \vdash \varphi \rightarrow \Finv x \, \psi \)
Proof
l0
nfd.1
\( \vdash \varphi \rightarrow \exists x \, \psi \rightarrow \forall x \, \psi \)
df-nf
\( \vdash \Finv x \, \psi \leftrightarrow \exists x \, \psi \rightarrow \forall x \, \psi \)
sylibr l0 _