Theorem nfbi 1821

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 1820	. 2 ⊢ (⊤ → Ⅎ𝑥(𝜑 ↔ 𝜓))
6	5	trud 1484	1 ⊢ Ⅎ𝑥(𝜑 ↔ 𝜓)

Syntax hints:   ↔ wb 195  ⊤wtru 1476  Ⅎwnf 1699

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

This theorem depends on definitions:  df-bi 196  df-or 384  df-an 385  df-tru 1478  df-ex 1696  df-nf 1701

This theorem is referenced by:  euf  2466  sb8eu  2491  bm1.1  2595  cleqh  2711  sbhypf  3226  ceqsexg  3304  elabgt  3316  elabgf  3317  axrep1  4700  axrep3  4702  axrep4  4703  copsex2t  4883  copsex2g  4884  opelopabsb  4910  opeliunxp2  5182  ralxpf  5190  cbviota  5773  sb8iota  5775  fvopab5  6217  fmptco  6303  nfiso  6472  dfoprab4f  7117  opeliunxp2f  7223  xpf1o  8007  zfcndrep  9315  gsumcom2  18197  isfildlem  21471  cnextfvval  21679  mbfsup  23237  mbfinf  23238  brabgaf  28800  fmptcof2  28839  bnj1468  30170  subtr2  31479  bj-abbi  31963  bj-axrep1  31976  bj-axrep3  31978  bj-axrep4  31979  mpt2bi123f  33141  dfcleqf  38281  fourierdlem31  39031