Theorem nfbi 1873

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

Syntax hints:   ↔ wb 196  ⊤wtru 1524  Ⅎwnf 1748

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

This theorem depends on definitions:  df-bi 197  df-or 384  df-an 385  df-tru 1526  df-ex 1745  df-nf 1750

This theorem is referenced by:  euf  2506  sb8eu  2532  bm1.1  2636  cleqh  2753  sbhypf  3284  ceqsexg  3365  elabgt  3379  elabgf  3380  axrep1  4805  axrep3  4807  axrep4  4808  copsex2t  4986  copsex2g  4987  opelopabsb  5014  opeliunxp2  5293  ralxpf  5301  cbviota  5894  sb8iota  5896  fvopab5  6349  fmptco  6436  nfiso  6612  dfoprab4f  7270  opeliunxp2f  7381  xpf1o  8163  zfcndrep  9474  gsumcom2  18420  isfildlem  21708  cnextfvval  21916  mbfsup  23476  mbfinf  23477  brabgaf  29546  fmptcof2  29585  bnj1468  31042  subtr2  32434  bj-abbi  32900  bj-axrep1  32913  bj-axrep3  32915  bj-axrep4  32916  mpt2bi123f  34101  eqrelf  34161  fourierdlem31  40673