Theorem nfan

If \( x \) is not free in \( \varphi \) and \( \psi \), then it is not free in \( \varphi \wedge \psi \). (Contributed by Mario Carneiro, 11-Aug-2016.) (Proof shortened by Wolf Lammen, 13-Jan-2018.) (Proof shortened by Wolf Lammen, 9-Oct-2021.)

Hypotheses
nfan.1
\( \vdash \Finv x \, \varphi \)
nfan.2
\( \vdash \Finv x \, \psi \)
Conclusion
\( \vdash \Finv x \, (\varphi \wedge \psi) \)
Proof
nfan.1
l1
a1i _
nfan.2
a1i _
nfand l1 _
mptru _