Theorem nfbi 1611

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

Syntax hints:   ↔ wb 105  ⊤wtru 1373  Ⅎwnf 1482

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 1469  ax-gen 1471  ax-4 1532  ax-ial 1556  ax-i5r 1557

This theorem depends on definitions:  df-bi 117  df-tru 1375  df-nf 1483

This theorem is referenced by:  sb8eu  2066  nfeuv  2071  bm1.1  2189  abbi  2318  nfeq  2355  cleqf  2372  sbhypf  2821  ceqsexg  2900  elabgt  2913  elabgf  2914  copsex2t  4288  copsex2g  4289  opelopabsb  4305  opeliunxp2  4817  ralxpf  4823  rexxpf  4824  cbviota  5236  sb8iota  5238  fmptco  5745  nfiso  5874  uchoice  6222  dfoprab4f  6278  opeliunxp2f  6323  xpf1o  6940  bdsepnfALT  15787