This is an inofficial mirror of http://metamath.tirix.org for personal testing of a visualizer extension only.

Metamath Proof Explorer

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	$⊢ φ \to Ⅎ x ψ$
	nfbid.2	$⊢ φ \to Ⅎ x χ$
Assertion	nfbid	$⊢ φ \to Ⅎ x (ψ \leftrightarrow χ)$

Proof

Step	Hyp	Ref	Expression
1		nfbid.1	$⊢ φ \to Ⅎ x ψ$
2		nfbid.2	$⊢ φ \to Ⅎ x χ$
3		dfbi2	$⊢ (ψ \leftrightarrow χ) \leftrightarrow ((ψ \to χ) \land (χ \to ψ))$
4	1 2	nfimd	$⊢ φ \to Ⅎ x (ψ \to χ)$
5	2 1	nfimd	$⊢ φ \to Ⅎ x (χ \to ψ)$
6	4 5	nfand	$⊢ φ \to Ⅎ x ((ψ \to χ) \land (χ \to ψ))$
7	3 6	nfxfrd	$⊢ φ \to Ⅎ x (ψ \leftrightarrow χ)$