Theorem nfbi 1589

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

Syntax hints:   ↔ wb 105  ⊤wtru 1354  Ⅎwnf 1460

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 1447  ax-gen 1449  ax-4 1510  ax-ial 1534  ax-i5r 1535

This theorem depends on definitions:  df-bi 117  df-tru 1356  df-nf 1461

This theorem is referenced by:  sb8eu  2039  nfeuv  2044  bm1.1  2162  abbi  2291  nfeq  2327  cleqf  2344  sbhypf  2786  ceqsexg  2865  elabgt  2878  elabgf  2879  copsex2t  4243  copsex2g  4244  opelopabsb  4258  opeliunxp2  4764  ralxpf  4770  rexxpf  4771  cbviota  5180  sb8iota  5182  fmptco  5679  nfiso  5802  dfoprab4f  6189  opeliunxp2f  6234  xpf1o  6839  bdsepnfALT  14412