Theorem nfbi 1911

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 1910	. 2 ⊢ (⊤ → Ⅎ𝑥(𝜑 ↔ 𝜓))
6	5	mptru 1555	1 ⊢ Ⅎ𝑥(𝜑 ↔ 𝜓)

Syntax hints:   ↔ wb 208  ⊤wtru 1549  Ⅎwnf 1791

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

This theorem depends on definitions:  df-bi 209  df-an 398  df-or 855  df-tru 1551  df-ex 1788  df-nf 1792

This theorem is referenced by:  sbbib  2371  euf  2582  sb8eulem  2604  axextmo  2717  abbib  2810  cleqh  2870  cleqf  2931  ceqsexg  3592  elabgf  3613  axrep1  5202  axrep3  5205  axrep4OLD  5208  copsex2t  5435  opeliunxp2  5782  ralxpf  5790  cbviotaw  6451  cbviota  6453  sb8iota  6455  fvopab5  6972  fmptco  7074  nfiso  7269  dfoprab4f  8000  opeliunxp2f  8152  xpf1o  9071  zfcndrep  10533  gsumcom2  19944  isfildlem  23843  cnextfvval  24051  mbfsup  25652  mbfinf  25653  brabgaf  32700  fmptcof2  32751  esplyfval1  33767  bnj1468  35041  subtr2  36556  bj-axseprep  37440  bj-axreprepsep  37441  mpobi123f  38542  eqrelf  38638  unielss  43676  permaxrep  45463  fourierdlem31  46593