Theorem nfbi 1635

Description: If 𝑥 is not free in 𝜑 and 𝜓, then 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 1634	. 2 ⊢ (⊤ → Ⅎ𝑥(𝜑 ↔ 𝜓))
6	5	mptru 1404	1 ⊢ Ⅎ𝑥(𝜑 ↔ 𝜓)

Syntax hints:   ↔ wb 105  ⊤wtru 1396  Ⅎwnf 1506

This theorem was proved from axioms:  ax-mp 5  ax-1 6  ax-2 7  ax-ia1 106  ax-ia2 107  ax-ia3 108  ax-5 1493  ax-gen 1495  ax-4 1556  ax-ial 1580  ax-i5r 1581

This theorem depends on definitions:  df-bi 117  df-tru 1398  df-nf 1507

This theorem is referenced by:  sb8eu  2090  nfeuv  2095  bm1.1  2214  abbi  2343  nfeq  2380  cleqf  2397  sbhypf  2851  ceqsexg  2932  elabgt  2945  elabgf  2946  copsex2t  4335  copsex2g  4336  opelopabsb  4352  opeliunxp2  4868  ralxpf  4874  rexxpf  4875  cbviota  5289  sb8iota  5292  fmptco  5809  nfiso  5942  uchoice  6295  dfoprab4f  6351  opeliunxp2f  6399  xpf1o  7025  bdsepnfALT  16420