Theorem nf5dh

Deduce that \( x \) is not free in \( \psi \) in a context. (Contributed by Mario Carneiro, 24-Sep-2016.) [df-nf] changed. (Revised by Wolf Lammen, 11-Oct-2021.)

Hypotheses
nf5dh.1
\( \vdash \varphi \rightarrow \forall x \, \varphi \)
nf5dh.2
\( \vdash \varphi \rightarrow \psi \rightarrow \forall x \, \psi \)
Conclusion
\( \vdash \varphi \rightarrow \Finv x \, \psi \)
Proof
l0
nf5dh.1
nf5dh.2
l2
alrimih l0 _
\( \vdash \varphi \rightarrow \forall x \, (\psi \rightarrow \forall x \, \psi) \)
nf5-1
\( \vdash \forall x \, (\psi \rightarrow \forall x \, \psi) \rightarrow \Finv x \, \psi \)
syl l2 _