Theorem nfbid

If in a context \( x \) is not free in \( \psi \) and \( \chi \), then it is not free in \( \psi \leftrightarrow \chi \). (Contributed by Mario Carneiro, 24-Sep-2016.) (Proof shortened by Wolf Lammen, 29-Dec-2017.)

Hypotheses
nfbid.1
\( \vdash \varphi \rightarrow \Finv x \, \psi \)
nfbid.2
\( \vdash \varphi \rightarrow \Finv x \, \chi \)
Conclusion
\( \vdash \varphi \rightarrow \Finv x \, (\psi \leftrightarrow \chi) \)
Proof
l0
dfbi2
\( \vdash \psi \leftrightarrow \chi \leftrightarrow (\psi \rightarrow \chi) \wedge (\chi \rightarrow \psi) \)
l1
nfbid.1
nfbid.2
l3
nfimd l1 _
l4
nfbid.2
nfbid.1
nfimd l4 _
nfand l3 _
\( \vdash \varphi \rightarrow \Finv x \, ((\psi \rightarrow \chi) \wedge (\chi \rightarrow \psi)) \)
nfxfrd l0 _