Theorem nf5dv

Apply the definition of not-free in a context. (Contributed by Mario Carneiro, 11-Aug-2016.) [df-nf] changed. (Revised by Wolf Lammen, 18-Sep-2021.) (Proof shortened by Wolf Lammen, 13-Jul-2022.)

Hypothesis
nf5dv.1
\( \vdash \varphi \rightarrow \psi \rightarrow \forall x \, \psi \)
Conclusion
\( \vdash \varphi \rightarrow \Finv x \, \psi \)
Proof
l0
ax-5
nf5dv.1
nf5dh l0 _