Theorem nfbi 1904

Description: If 𝑥 is not free in 𝜑 and 𝜓, then 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 1903	. 2 ⊢ (⊤ → Ⅎ𝑥(𝜑 ↔ 𝜓))
6	5	mptru 1548	1 ⊢ Ⅎ𝑥(𝜑 ↔ 𝜓)

Syntax hints:   ↔ wb 206  ⊤wtru 1542  Ⅎwnf 1784

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

This theorem depends on definitions:  df-bi 207  df-an 396  df-or 848  df-tru 1544  df-ex 1781  df-nf 1785

This theorem is referenced by:  sbbib  2361  euf  2571  sb8eulem  2593  axextmo  2707  abbib  2800  cleqh  2860  cleqf  2923  ceqsexg  3603  elabgf  3625  axrep1  5216  axrep3  5219  axrep4OLD  5222  copsex2t  5430  opeliunxp2  5777  ralxpf  5785  cbviotaw  6444  cbviota  6446  sb8iota  6448  fvopab5  6962  fmptco  7062  nfiso  7256  dfoprab4f  7988  opeliunxp2f  8140  xpf1o  9052  zfcndrep  10505  gsumcom2  19887  isfildlem  23772  cnextfvval  23980  mbfsup  25592  mbfinf  25593  brabgaf  32589  fmptcof2  32639  bnj1468  34858  subtr2  36359  mpobi123f  38212  eqrelf  38302  unielss  43321  permaxrep  45109  fourierdlem31  46246