Theorem nf3an

If \( x \) is not free in \( \varphi \), \( \psi \), and \( \chi \), then it is not free in \( \varphi \wedge \psi \wedge \chi \). (Contributed by Mario Carneiro, 11-Aug-2016.)

Hypotheses
nfan.1
\( \vdash \Finv x \, \varphi \)
nfan.2
\( \vdash \Finv x \, \psi \)
nfan.3
\( \vdash \Finv x \, \chi \)
Conclusion
\( \vdash \Finv x \, (\varphi \wedge \psi \wedge \chi) \)
Proof
l0
df-3an
\( \vdash \varphi \wedge \psi \wedge \chi \leftrightarrow \varphi \wedge \psi \wedge \chi \)
l1
nfan.1
nfan.2
l3
nfan l1 _
nfan.3
nfan l3 _
\( \vdash \Finv x \, (\varphi \wedge \psi \wedge \chi) \)
nfxfr l0 _