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