Theorem nf3or

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

Hypotheses
nf.1
\( \vdash \Finv x \, \varphi \)
nf.2
\( \vdash \Finv x \, \psi \)
nf.3
\( \vdash \Finv x \, \chi \)
Conclusion
\( \vdash \Finv x \, (\varphi \vee \psi \vee \chi) \)
Proof
l0
df-3or
\( \vdash \varphi \vee \psi \vee \chi \leftrightarrow \varphi \vee \psi \vee \chi \)
l1
nf.1
nf.2
l3
nfor l1 _
nf.3
nfor l3 _
\( \vdash \Finv x \, (\varphi \vee \psi \vee \chi) \)
nfxfr l0 _