Theorem nfbi 1521

Description: If 𝑥 is not free in 𝜑 and 𝜓, it is not free in (𝜑 ↔ 𝜓). (Contributed by Mario Carneiro, 11-Aug-2016.) (Proof shortened by Wolf Lammen, 2-Jan-2018.)

Hypotheses

Ref	Expression
nfbi.1	⊢ Ⅎ𝑥𝜑
nfbi.2	⊢ Ⅎ𝑥𝜓

Assertion

Ref	Expression
nfbi	⊢ Ⅎ𝑥(𝜑 ↔ 𝜓)

Proof of Theorem nfbi

Step	Hyp	Ref	Expression
1		nfbi.1	. . . 4 ⊢ Ⅎ𝑥𝜑
2	1	a1i 9	. . 3 ⊢ (⊤ → Ⅎ𝑥𝜑)
3		nfbi.2	. . . 4 ⊢ Ⅎ𝑥𝜓
4	3	a1i 9	. . 3 ⊢ (⊤ → Ⅎ𝑥𝜓)
5	2, 4	nfbid 1520	. 2 ⊢ (⊤ → Ⅎ𝑥(𝜑 ↔ 𝜓))
6	5	trud 1293	1 ⊢ Ⅎ𝑥(𝜑 ↔ 𝜓)

Syntax hints:   ↔ wb 103  ⊤wtru 1285  Ⅎwnf 1389

This theorem was proved from axioms:  ax-1 5  ax-2 6  ax-mp 7  ax-ia1 104  ax-ia2 105  ax-ia3 106  ax-5 1376  ax-gen 1378  ax-4 1440  ax-ial 1467  ax-i5r 1468

This theorem depends on definitions:  df-bi 115  df-tru 1287  df-nf 1390

This theorem is referenced by:  sb8eu  1954  nfeuv  1959  bm1.1  2066  abbi  2192  nfeq  2226  cleqf  2242  sbhypf  2648  ceqsexg  2723  elabgt  2735  elabgf  2736  copsex2t  4000  copsex2g  4001  opelopabsb  4015  opeliunxp2  4494  ralxpf  4500  rexxpf  4501  cbviota  4892  sb8iota  4894  fmptco  5351  nfiso  5466  dfoprab4f  5839  bdsepnfALT  10680  strcollnfALT  10781