Theorem nfan1

A closed form of nfan. (Contributed by Mario Carneiro, 3-Oct-2016.) [df-nf] changed. (Revised by Wolf Lammen, 18-Sep-2021.) (Proof shortened by Wolf Lammen, 7-Jul-2022.)

Hypotheses
nfim1.1
\( \vdash \Finv x \, \varphi \)
nfim1.2
\( \vdash \varphi \rightarrow \Finv x \, \psi \)
Conclusion
\( \vdash \Finv x \, (\varphi \wedge \psi) \)
Proof
l0
df-an
\( \vdash \varphi \wedge \psi \leftrightarrow \neg (\varphi \rightarrow \neg \psi) \)
l1
nfim1.1
nfim1.2
nfnd _
nfim1 l1 _
nfn _
\( \vdash \Finv x \, (\neg (\varphi \rightarrow \neg \psi)) \)
nfxfr l0 _