Theorem nfbid 1934

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 480	. 2 ⊢ ((𝜓 ↔ 𝜒) ↔ ((𝜓 → 𝜒) ∧ (𝜒 → 𝜓)))
2		nfbid.1	. . . 4 ⊢ (𝜑 → Ⅎ𝑥𝜓)
3		nfbid.2	. . . 4 ⊢ (𝜑 → Ⅎ𝑥𝜒)
4	2, 3	nfimd 1926	. . 3 ⊢ (𝜑 → Ⅎ𝑥(𝜓 → 𝜒))
5	3, 2	nfimd 1926	. . 3 ⊢ (𝜑 → Ⅎ𝑥(𝜒 → 𝜓))
6	4, 5	nfand 1929	. 2 ⊢ (𝜑 → Ⅎ𝑥((𝜓 → 𝜒) ∧ (𝜒 → 𝜓)))
7	1, 6	nfxfrd 1886	1 ⊢ (𝜑 → Ⅎ𝑥(𝜓 ↔ 𝜒))

This proof depends on syntax axioms:   → wi 4   ↔ wb 209   ∧ wa 401  Ⅎwnf 1815

This proof depends on axioms:  ax-mp 5  ax-1 6  ax-2 7  ax-3 8  ax-gen 1827  ax-4 1841

This proof depends on definitions:  df-bi 210  df-an 402  df-or 862  df-ex 1812  df-nf 1816

This theorem is used by:  nfbi  1935  nfeqd  2932  nfiotadw  6497  nfiotad  6499  iota2df  6525  axextnd  10677  axrepndlem1  10678  axrepndlem2  10679  axacndlem4  10696  axacndlem5  10697  axacnd  10698  axsepg2  35857  axsepg3  35858  axsepg3ALT  35859  axsepg5  35861  axextdist  36636  copsex2d  38136  cbveud  38371  wl-eudf  38580  wl-sb8eut  38586  wl-sb8eutv  38587