Theorem nfbi 1613

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

Syntax hints:   ↔ wb 105  ⊤wtru 1374  Ⅎwnf 1484

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 1471  ax-gen 1473  ax-4 1534  ax-ial 1558  ax-i5r 1559

This theorem depends on definitions:  df-bi 117  df-tru 1376  df-nf 1485

This theorem is referenced by:  sb8eu  2068  nfeuv  2073  bm1.1  2192  abbi  2321  nfeq  2358  cleqf  2375  sbhypf  2827  ceqsexg  2908  elabgt  2921  elabgf  2922  copsex2t  4307  copsex2g  4308  opelopabsb  4324  opeliunxp2  4836  ralxpf  4842  rexxpf  4843  cbviota  5256  sb8iota  5258  fmptco  5769  nfiso  5898  uchoice  6246  dfoprab4f  6302  opeliunxp2f  6347  xpf1o  6966  bdsepnfALT  16024