Theorem nfbid 1902

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

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

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

This theorem depends on definitions:  df-bi 207  df-an 396  df-or 848  df-ex 1780  df-nf 1784

This theorem is referenced by:  nfbi  1903  nfeqd  2902  nfiotadw  6467  nfiotad  6469  iota2df  6498  axextnd  10544  axrepndlem1  10545  axrepndlem2  10546  axacndlem4  10563  axacndlem5  10564  axacnd  10565  axsepg2  35072  axsepg2ALT  35073  axextdist  35787  copsex2d  37127  cbveud  37360  wl-eudf  37560  wl-sb8eut  37566  wl-sb8eutv  37567