Theorem nfbi 1600

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

Syntax hints:   ↔ wb 105  ⊤wtru 1365  Ⅎwnf 1471

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 1458  ax-gen 1460  ax-4 1521  ax-ial 1545  ax-i5r 1546

This theorem depends on definitions:  df-bi 117  df-tru 1367  df-nf 1472

This theorem is referenced by:  sb8eu  2055  nfeuv  2060  bm1.1  2178  abbi  2307  nfeq  2344  cleqf  2361  sbhypf  2810  ceqsexg  2889  elabgt  2902  elabgf  2903  copsex2t  4275  copsex2g  4276  opelopabsb  4291  opeliunxp2  4803  ralxpf  4809  rexxpf  4810  cbviota  5221  sb8iota  5223  fmptco  5725  nfiso  5850  uchoice  6192  dfoprab4f  6248  opeliunxp2f  6293  xpf1o  6902  bdsepnfALT  15451