Theorem nfand

If in a context \( x \) is not free in \( \psi \) and \( \chi \), then it is not free in \( \psi \wedge \chi \). (Contributed by Mario Carneiro, 7-Oct-2016.)

Hypotheses
nfand.1
\( \vdash \varphi \rightarrow \Finv x \, \psi \)
nfand.2
\( \vdash \varphi \rightarrow \Finv x \, \chi \)
Conclusion
\( \vdash \varphi \rightarrow \Finv x \, (\psi \wedge \chi) \)
Proof
l0
df-an
\( \vdash \psi \wedge \chi \leftrightarrow \neg (\psi \rightarrow \neg \chi) \)
l1
nfand.1
nfand.2
nfnd _
nfimd l1 _
nfnd _
\( \vdash \varphi \rightarrow \Finv x \, (\neg (\psi \rightarrow \neg \chi)) \)
nfxfrd l0 _