Theorem nfbi 1637

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 1636	. 2 ⊢ (⊤ → Ⅎ𝑥(𝜑 ↔ 𝜓))
6	5	mptru 1406	1 ⊢ Ⅎ𝑥(𝜑 ↔ 𝜓)

Syntax hints:   ↔ wb 105  ⊤wtru 1398  Ⅎwnf 1508

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 1495  ax-gen 1497  ax-4 1558  ax-ial 1582  ax-i5r 1583

This theorem depends on definitions:  df-bi 117  df-tru 1400  df-nf 1509

This theorem is referenced by:  sb8eu  2092  nfeuv  2097  bm1.1  2216  abbi  2345  nfeq  2382  cleqf  2399  sbhypf  2853  ceqsexg  2934  elabgt  2947  elabgf  2948  copsex2t  4337  copsex2g  4338  opelopabsb  4354  opeliunxp2  4870  ralxpf  4876  rexxpf  4877  cbviota  5291  sb8iota  5294  fmptco  5813  nfiso  5946  uchoice  6299  dfoprab4f  6355  opeliunxp2f  6403  xpf1o  7029  bdsepnfALT  16484