Theorem nfbid 1931

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

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

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

This proof depends on definitions:  df-bi 210  df-an 401  df-or 861  df-ex 1809  df-nf 1813

This theorem is used by:  nfbi  1932  nfeqd  2934  nfiotadw  6495  nfiotad  6497  iota2df  6523  axextnd  10582  axrepndlem1  10583  axrepndlem2  10584  axacndlem4  10601  axacndlem5  10602  axacnd  10603  axsepg2  35561  axsepg3  35562  axsepg3ALT  35563  axsepg5  35565  axextdist  36297  copsex2d  37811  cbveud  38046  wl-eudf  38255  wl-sb8eut  38261  wl-sb8eutv  38262