Theorem nfor

If \( x \) is not free in \( \varphi \) and \( \psi \), then it is not free in \( \varphi \vee \psi \). (Contributed by NM, 5-Aug-1993.) (Revised by Mario Carneiro, 11-Aug-2016.)

Hypotheses
nf.1
\( \vdash \Finv x \, \varphi \)
nf.2
\( \vdash \Finv x \, \psi \)
Conclusion
\( \vdash \Finv x \, (\varphi \vee \psi) \)
Proof
l0
df-or
\( \vdash \varphi \vee \psi \leftrightarrow \neg \varphi \rightarrow \psi \)
nf.1
l2
nfn _
nf.2
nfim l2 _
\( \vdash \Finv x \, (\neg \varphi \rightarrow \psi) \)
nfxfr l0 _