Theorem nfbid 1916

Description: If in a context 𝑥 is not free in 𝜓 and 𝜒, then it is not free in (𝜓 ↔ 𝜒). (Contributed by Mario Carneiro, 24-Sep-2016.) (Proof shortened by Wolf Lammen, 29-Dec-2017.)

Hypotheses

Ref	Expression
nfbid.1	⊢ (𝜑 → Ⅎ𝑥𝜓)
nfbid.2	⊢ (𝜑 → Ⅎ𝑥𝜒)

Assertion

Ref	Expression
nfbid	⊢ (𝜑 → Ⅎ𝑥(𝜓 ↔ 𝜒))

Proof of Theorem nfbid

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

Syntax hints:   → wi 4   ↔ wb 208   ∧ wa 398  Ⅎwnf 1797

This theorem was proved from axioms:  ax-mp 5  ax-1 6  ax-2 7  ax-3 8  ax-gen 1809  ax-4 1823

This theorem depends on definitions:  df-bi 209  df-an 399  df-or 857  df-ex 1794  df-nf 1798

This theorem is referenced by:  nfbi  1917  nfeqd  2928  nfiotadw  6469  nfiotad  6471  iota2df  6497  axextnd  10539  axrepndlem1  10540  axrepndlem2  10541  axacndlem4  10558  axacndlem5  10559  axacnd  10560  axsepg2  35391  axsepg3  35392  axsepg3ALT  35393  axsepg5  35395  axextdist  36095  copsex2d  37579  cbveud  37814  wl-eudf  38023  wl-sb8eut  38029  wl-sb8eutv  38030