Theorem nfbi

If \( x \) is not free in \( \varphi \) and \( \psi \), then it is not free in \( \varphi \leftrightarrow \psi \). (Contributed by NM, 26-May-1993.) (Revised by Mario Carneiro, 11-Aug-2016.) (Proof shortened by Wolf Lammen, 2-Jan-2018.)

Hypotheses
nf.1
\( \vdash \Finv x \, \varphi \)
nf.2
\( \vdash \Finv x \, \psi \)
Conclusion
\( \vdash \Finv x \, (\varphi \leftrightarrow \psi) \)
Proof
nf.1
l1
a1i _
nf.2
a1i _
nfbid l1 _
mptru _