Theorem nfbid 1930

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 1922	. . 3 ⊢ (𝜑 → Ⅎ𝑥(𝜓 → 𝜒))
5	3, 2	nfimd 1922	. . 3 ⊢ (𝜑 → Ⅎ𝑥(𝜒 → 𝜓))
6	4, 5	nfand 1925	. 2 ⊢ (𝜑 → Ⅎ𝑥((𝜓 → 𝜒) ∧ (𝜒 → 𝜓)))
7	1, 6	nfxfrd 1882	1 ⊢ (𝜑 → Ⅎ𝑥(𝜓 ↔ 𝜒))

Syntax hints:   → wi 4   ↔ wb 209   ∧ wa 400  Ⅎwnf 1811

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

This theorem depends on definitions:  df-bi 210  df-an 401  df-or 861  df-ex 1808  df-nf 1812

This theorem is referenced by:  nfbi  1931  nfeqd  2933  nfiotadw  6495  nfiotad  6497  iota2df  6523  axextnd  10575  axrepndlem1  10576  axrepndlem2  10577  axacndlem4  10594  axacndlem5  10595  axacnd  10596  axsepg2  35519  axsepg3  35520  axsepg3ALT  35521  axsepg5  35523  axextdist  36255  copsex2d  37749  cbveud  37984  wl-eudf  38193  wl-sb8eut  38199  wl-sb8eutv  38200