Theorem nfnd

Deduction associated with nfnt. (Contributed by Mario Carneiro, 24-Sep-2016.)

Hypothesis
nfnd.1
\( \vdash \varphi \rightarrow \Finv x \, \psi \)
Conclusion
\( \vdash \varphi \rightarrow \Finv x \, (\neg \psi) \)
Proof
l0
nfnd.1
\( \vdash \varphi \rightarrow \Finv x \, \psi \)
nfnt
\( \vdash \Finv x \, \psi \rightarrow \Finv x \, (\neg \psi) \)
syl l0 _