Theorem nfbi 1833

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

Syntax hints:   ↔ wb 196  ⊤wtru 1484  Ⅎwnf 1708

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

This theorem depends on definitions:  df-bi 197  df-or 385  df-an 386  df-tru 1486  df-ex 1705  df-nf 1710

This theorem is referenced by:  euf  2478  sb8eu  2503  bm1.1  2607  cleqh  2724  sbhypf  3253  ceqsexg  3334  elabgt  3347  elabgf  3348  axrep1  4772  axrep3  4774  axrep4  4775  copsex2t  4957  copsex2g  4958  opelopabsb  4985  opeliunxp2  5260  ralxpf  5268  cbviota  5856  sb8iota  5858  fvopab5  6309  fmptco  6396  nfiso  6572  dfoprab4f  7226  opeliunxp2f  7336  xpf1o  8122  zfcndrep  9436  gsumcom2  18374  isfildlem  21661  cnextfvval  21869  mbfsup  23431  mbfinf  23432  brabgaf  29420  fmptcof2  29457  bnj1468  30916  subtr2  32309  bj-abbi  32775  bj-axrep1  32788  bj-axrep3  32790  bj-axrep4  32791  mpt2bi123f  33971  eqrelf  34020  fourierdlem31  40355