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	|- ( ph -> F/ x ps )
	nfbid.2	|- ( ph -> F/ x ch )
Assertion	nfbid	|- ( ph -> F/ x ( ps <-> ch ) )

Proof

Step	Hyp	Ref	Expression
1		nfbid.1	|- ( ph -> F/ x ps )
2		nfbid.2	|- ( ph -> F/ x ch )
3		dfbi2	|- ( ( ps <-> ch ) <-> ( ( ps -> ch ) /\ ( ch -> ps ) ) )
4	1 2	nfimd	|- ( ph -> F/ x ( ps -> ch ) )
5	2 1	nfimd	|- ( ph -> F/ x ( ch -> ps ) )
6	4 5	nfand	|- ( ph -> F/ x ( ( ps -> ch ) /\ ( ch -> ps ) ) )
7	3 6	nfxfrd	|- ( ph -> F/ x ( ps <-> ch ) )