Theorem nfbid 1904

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 474	. 2 ⊢ ((𝜓 ↔ 𝜒) ↔ ((𝜓 → 𝜒) ∧ (𝜒 → 𝜓)))
2		nfbid.1	. . . 4 ⊢ (𝜑 → Ⅎ𝑥𝜓)
3		nfbid.2	. . . 4 ⊢ (𝜑 → Ⅎ𝑥𝜒)
4	2, 3	nfimd 1896	. . 3 ⊢ (𝜑 → Ⅎ𝑥(𝜓 → 𝜒))
5	3, 2	nfimd 1896	. . 3 ⊢ (𝜑 → Ⅎ𝑥(𝜒 → 𝜓))
6	4, 5	nfand 1899	. 2 ⊢ (𝜑 → Ⅎ𝑥((𝜓 → 𝜒) ∧ (𝜒 → 𝜓)))
7	1, 6	nfxfrd 1856	1 ⊢ (𝜑 → Ⅎ𝑥(𝜓 ↔ 𝜒))

Syntax hints:   → wi 4   ↔ wb 206   ∧ wa 395  Ⅎwnf 1785

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

This theorem depends on definitions:  df-bi 207  df-an 396  df-or 849  df-ex 1782  df-nf 1786

This theorem is referenced by:  nfbi  1905  nfeqd  2910  nfiotadw  6459  nfiotad  6461  iota2df  6487  axextnd  10514  axrepndlem1  10515  axrepndlem2  10516  axacndlem4  10533  axacndlem5  10534  axacnd  10535  axsepg2  35257  axsepg2ALT  35258  axextdist  36010  copsex2d  37383  cbveud  37616  wl-eudf  37816  wl-sb8eut  37822  wl-sb8eutv  37823