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

Metamath Proof Explorer

Theorem nfbi

Description: If x is not free in ph and ps , then it is not free in ( ph <-> ps ) . (Contributed by NM, 26-May-1993) (Revised by Mario Carneiro, 11-Aug-2016) (Proof shortened by Wolf Lammen, 2-Jan-2018)

	Ref	Expression
Hypotheses	nf.1	⊢ Ⅎ 𝑥 𝜑
	nf.2	⊢ Ⅎ 𝑥 𝜓
Assertion	nfbi	⊢ Ⅎ 𝑥 ( 𝜑 ↔ 𝜓 )

Proof

Step	Hyp	Ref	Expression
1		nf.1	⊢ Ⅎ 𝑥 𝜑
2		nf.2	⊢ Ⅎ 𝑥 𝜓
3	1	a1i	⊢ ( ⊤ → Ⅎ 𝑥 𝜑 )
4	2	a1i	⊢ ( ⊤ → Ⅎ 𝑥 𝜓 )
5	3 4	nfbid	⊢ ( ⊤ → Ⅎ 𝑥 ( 𝜑 ↔ 𝜓 ) )
6	5	mptru	⊢ Ⅎ 𝑥 ( 𝜑 ↔ 𝜓 )