Theorem nfbi 1933

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

Syntax hints:   ↔ wb 209  ⊤wtru 1571  Ⅎwnf 1813

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

This theorem depends on definitions:  df-bi 210  df-an 401  df-or 861  df-tru 1573  df-ex 1810  df-nf 1814

This theorem is referenced by:  sbbib  2393  euf  2604  sb8eulem  2626  axextmo  2739  abbib  2832  cleqh  2892  cleqf  2953  ceqsexg  3612  elabgf  3633  axrep1  5239  axrep3  5242  axrep4OLD  5245  copsex2t  5475  opeliunxp2  5824  ralxpf  5832  cbviotaw  6499  cbviota  6501  sb8iota  6503  fvopab5  7023  fmptco  7125  nfiso  7320  dfoprab4f  8049  opeliunxp2f  8202  xpf1o  9123  zfcndrep  10594  gsumcom2  20040  isfildlem  24014  cnextfvval  24222  mbfsup  25823  mbfinf  25824  brabgaf  32951  fmptcof2  33002  esplyfval1  33963  bnj1468  35234  subtr2  36846  bj-axseprep  37731  bj-axreprepsep  37732  mpobi123f  38831  eqrelf  38927  unielss  43965  permaxrep  45735  fourierdlem31  46872