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	⊢ ( 𝜑 → Ⅎ 𝑥 𝜓 )
	nfbid.2	⊢ ( 𝜑 → Ⅎ 𝑥 𝜒 )
Assertion	nfbid	⊢ ( 𝜑 → Ⅎ 𝑥 ( 𝜓 ↔ 𝜒 ) )

Proof

Step	Hyp	Ref	Expression
1		nfbid.1	⊢ ( 𝜑 → Ⅎ 𝑥 𝜓 )
2		nfbid.2	⊢ ( 𝜑 → Ⅎ 𝑥 𝜒 )
3		dfbi2	⊢ ( ( 𝜓 ↔ 𝜒 ) ↔ ( ( 𝜓 → 𝜒 ) ∧ ( 𝜒 → 𝜓 ) ) )
4	1 2	nfimd	⊢ ( 𝜑 → Ⅎ 𝑥 ( 𝜓 → 𝜒 ) )
5	2 1	nfimd	⊢ ( 𝜑 → Ⅎ 𝑥 ( 𝜒 → 𝜓 ) )
6	4 5	nfand	⊢ ( 𝜑 → Ⅎ 𝑥 ( ( 𝜓 → 𝜒 ) ∧ ( 𝜒 → 𝜓 ) ) )
7	3 6	nfxfrd	⊢ ( 𝜑 → Ⅎ 𝑥 ( 𝜓 ↔ 𝜒 ) )