Theorem nfbid

Description: If in a context x is not free in ps and ch , then it is not free in ( ps <-> ch ) . (Contributed by Mario Carneiro, 24-Sep-2016) (Proof shortened by Wolf Lammen, 29-Dec-2017)

	Ref	Expression
Hypotheses	nfbid.1	$$⊢\phi \to Ⅎx\psi$$
	nfbid.2	$$⊢\phi \to Ⅎx\chi$$
Assertion	nfbid	$$⊢\phi \to Ⅎx\left(\psi \leftrightarrow \chi \right)$$

Proof

Step	Hyp	Ref	Expression
1		nfbid.1	$$⊢\phi \to Ⅎx\psi$$
2		nfbid.2	$$⊢\phi \to Ⅎx\chi$$
3		dfbi2	$$⊢\left(\psi \leftrightarrow \chi \right)\leftrightarrow \left(\left(\psi \to \chi \right)\wedge \left(\chi \to \psi \right)\right)$$
4	1 2	nfimd	$$⊢\phi \to Ⅎx\left(\psi \to \chi \right)$$
5	2 1	nfimd	$$⊢\phi \to Ⅎx\left(\chi \to \psi \right)$$
6	4 5	nfand	$$⊢\phi \to Ⅎx\left(\left(\psi \to \chi \right)\wedge \left(\chi \to \psi \right)\right)$$
7	3 6	nfxfrd	$$⊢\phi \to Ⅎx\left(\psi \leftrightarrow \chi \right)$$