Theorem nf5d

Deduce that \( x \) is not free in \( \psi \) in a context. (Contributed by Mario Carneiro, 24-Sep-2016.)

Hypotheses
nf5d.1
\( \vdash \Finv x \, \varphi \)
nf5d.2
\( \vdash \varphi \rightarrow \psi \rightarrow \forall x \, \psi \)
Conclusion
\( \vdash \varphi \rightarrow \Finv x \, \psi \)
Proof
l0
nf5d.1
nf5d.2
l2
alrimi 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 _