Theorem nfbi 1582

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

Syntax hints:   ↔ wb 104  ⊤wtru 1349  Ⅎwnf 1453

This theorem was proved from axioms:  ax-mp 5  ax-1 6  ax-2 7  ax-ia1 105  ax-ia2 106  ax-ia3 107  ax-5 1440  ax-gen 1442  ax-4 1503  ax-ial 1527  ax-i5r 1528

This theorem depends on definitions:  df-bi 116  df-tru 1351  df-nf 1454

This theorem is referenced by:  sb8eu  2032  nfeuv  2037  bm1.1  2155  abbi  2284  nfeq  2320  cleqf  2337  sbhypf  2779  ceqsexg  2858  elabgt  2871  elabgf  2872  copsex2t  4228  copsex2g  4229  opelopabsb  4243  opeliunxp2  4749  ralxpf  4755  rexxpf  4756  cbviota  5163  sb8iota  5165  fmptco  5659  nfiso  5782  dfoprab4f  6169  opeliunxp2f  6214  xpf1o  6818  bdsepnfALT  13884