Theorem nfbi 1834

Description: If x is not free in φ and ψ, it is not free in (φ ↔ ψ). (Contributed by Mario Carneiro, 11-Aug-2016.) (Proof shortened by Wolf Lammen, 2-Jan-2018.)

Hypotheses

Ref	Expression
nf.1	⊢ Ⅎxφ
nf.2	⊢ Ⅎxψ

Assertion

Ref	Expression
nfbi	⊢ Ⅎx(φ ↔ ψ)

Proof of Theorem nfbi

Step	Hyp	Ref	Expression
1		nf.1	. . . 4 ⊢ Ⅎxφ
2	1	a1i 10	. . 3 ⊢ ( ⊤ → Ⅎxφ)
3		nf.2	. . . 4 ⊢ Ⅎxψ
4	3	a1i 10	. . 3 ⊢ ( ⊤ → Ⅎxψ)
5	2, 4	nfbid 1832	. 2 ⊢ ( ⊤ → Ⅎx(φ ↔ ψ))
6	5	trud 1323	1 ⊢ Ⅎx(φ ↔ ψ)

Syntax hints:   ↔ wb 176   ⊤ wtru 1316  Ⅎwnf 1544

This theorem was proved from axioms:  ax-mp 5  ax-1 6  ax-2 7  ax-3 8  ax-gen 1546  ax-5 1557  ax-17 1616  ax-9 1654  ax-8 1675  ax-6 1729  ax-11 1746

This theorem depends on definitions:  df-bi 177  df-an 360  df-tru 1319  df-ex 1542  df-nf 1545

This theorem is referenced by:  euf  2210  sb8eu  2222  bm1.1  2338  abbi  2464  nfeq  2497  cleqf  2514  sbhypf  2905  ceqsexg  2971  elabgt  2983  elabgf  2984  cbviota  4345  sb8iota  4347  copsex2t  4609  copsex2g  4610  opelopabsb  4698  opeliunxp2  4823  ralxpf  4828  nfiso  5488