Theorem nfbi 1830

Description: If 𝑥 is not free in 𝜑 and 𝜓, it is not free in (𝜑 ↔ 𝜓). (Contributed by NM, 26-May-1993.) (Revised by Mario Carneiro, 11-Aug-2016.) (Proof shortened by Wolf Lammen, 2-Jan-2018.)

Hypotheses

Ref	Expression
nf.1	⊢ Ⅎ𝑥𝜑
nf.2	⊢ Ⅎ𝑥𝜓

Assertion

Ref	Expression
nfbi	⊢ Ⅎ𝑥(𝜑 ↔ 𝜓)

Proof of Theorem nfbi

Step	Hyp	Ref	Expression
1		nf.1	. . . 4 ⊢ Ⅎ𝑥𝜑
2	1	a1i 11	. . 3 ⊢ (⊤ → Ⅎ𝑥𝜑)
3		nf.2	. . . 4 ⊢ Ⅎ𝑥𝜓
4	3	a1i 11	. . 3 ⊢ (⊤ → Ⅎ𝑥𝜓)
5	2, 4	nfbid 1829	. 2 ⊢ (⊤ → Ⅎ𝑥(𝜑 ↔ 𝜓))
6	5	trud 1490	1 ⊢ Ⅎ𝑥(𝜑 ↔ 𝜓)

Syntax hints:   ↔ wb 196  ⊤wtru 1481  Ⅎwnf 1705

This theorem was proved from axioms:  ax-mp 5  ax-1 6  ax-2 7  ax-3 8  ax-gen 1719  ax-4 1734

This theorem depends on definitions:  df-bi 197  df-or 385  df-an 386  df-tru 1483  df-ex 1702  df-nf 1707

This theorem is referenced by:  euf  2477  sb8eu  2502  bm1.1  2606  cleqh  2721  sbhypf  3243  ceqsexg  3322  elabgt  3335  elabgf  3336  axrep1  4742  axrep3  4744  axrep4  4745  copsex2t  4927  copsex2g  4928  opelopabsb  4955  opeliunxp2  5230  ralxpf  5238  cbviota  5825  sb8iota  5827  fvopab5  6275  fmptco  6362  nfiso  6537  dfoprab4f  7186  opeliunxp2f  7296  xpf1o  8082  zfcndrep  9396  gsumcom2  18314  isfildlem  21601  cnextfvval  21809  mbfsup  23371  mbfinf  23372  brabgaf  29304  fmptcof2  29340  bnj1468  30677  subtr2  32004  bj-abbi  32471  bj-axrep1  32484  bj-axrep3  32486  bj-axrep4  32487  mpt2bi123f  33642  fourierdlem31  39692