Theorem nfnan

If \( x \) is not free in \( \varphi \) and \( \psi \), then it is not free in \( \varphi \barwedge \psi \). (Contributed by Scott Fenton, 2-Jan-2018.)

Hypotheses
nfan.1
\( \vdash \Finv x \, \varphi \)
nfan.2
\( \vdash \Finv x \, \psi \)
Conclusion
\( \vdash \Finv x \, (\varphi \barwedge \psi) \)
Proof
l0
df-nan
\( \vdash \varphi \barwedge \psi \leftrightarrow \neg (\varphi \wedge \psi) \)
l1
nfan.1
nfan.2
nfan l1 _
nfn _
\( \vdash \Finv x \, (\neg (\varphi \wedge \psi)) \)
nfxfr l0 _