Theorem nfn

Inference associated with nfnt. (Contributed by Mario Carneiro, 11-Aug-2016.) [df-nf] changed. (Revised by Wolf Lammen, 18-Sep-2021.)

Hypothesis
nfn.1
\( \vdash \Finv x \, \varphi \)
Conclusion
\( \vdash \Finv x \, (\neg \varphi) \)
Proof
l0
nfn.1
\( \vdash \Finv x \, \varphi \)
nfnt
\( \vdash \Finv x \, \varphi \rightarrow \Finv x \, (\neg \varphi) \)
ax-mp l0 _