Theorem nfbi 1612

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

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

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 1470  ax-gen 1472  ax-4 1533  ax-ial 1557  ax-i5r 1558

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

This theorem is referenced by:  sb8eu  2067  nfeuv  2072  bm1.1  2190  abbi  2319  nfeq  2356  cleqf  2373  sbhypf  2822  ceqsexg  2901  elabgt  2914  elabgf  2915  copsex2t  4289  copsex2g  4290  opelopabsb  4306  opeliunxp2  4818  ralxpf  4824  rexxpf  4825  cbviota  5237  sb8iota  5239  fmptco  5746  nfiso  5875  uchoice  6223  dfoprab4f  6279  opeliunxp2f  6324  xpf1o  6941  bdsepnfALT  15825