Theorem nf5rd

Consequence of the definition of not-free in a context. (Contributed by Mario Carneiro, 11-Aug-2016.)

Hypothesis
nf5rd.1
\( \vdash \varphi \rightarrow \Finv x \, \psi \)
Conclusion
\( \vdash \varphi \rightarrow \psi \rightarrow \forall x \, \psi \)
Proof
l0
nf5rd.1
\( \vdash \varphi \rightarrow \Finv x \, \psi \)
nf5r
\( \vdash \Finv x \, \psi \rightarrow \psi \rightarrow \forall x \, \psi \)
syl l0 _