Theorem nfbi 1936

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

This proof depends on syntax axioms:   ↔ wb 209  ⊤wtru 1571  Ⅎwnf 1816

This proof depends on axioms:  ax-mp 5  ax-1 6  ax-2 7  ax-3 8  ax-gen 1828  ax-4 1842

This proof depends on definitions:  df-bi 210  df-an 402  df-or 862  df-tru 1573  df-ex 1813  df-nf 1817

This theorem is used by:  sbbib  2391  euf  2602  sb8eulem  2624  axextmo  2737  abbib  2830  cleqh  2890  cleqf  2951  ceqsexg  3607  elabgf  3628  axrep1  5233  axrep3  5236  copsex2t  5464  opeliunxp2  5815  ralxpf  5824  cbviotaw  6501  cbviota  6503  sb8iota  6505  fvopab5  7027  fmptco  7130  nfiso  7330  dfoprab4f  8067  opeliunxp2f  8227  xpf1o  9158  zfcndrep  10699  gsumcom2  20189  isfildlem  24176  cnextfvval  24384  mbfsup  25985  mbfinf  25986  brabgaf  33200  fmptcof2  33251  esplyfval1  34205  bnj1468  35476  subtr2  37103  bj-axseprep  37990  bj-axreprepsep  37991  mpobi123f  39094  eqrelf  39190  unielss  44219  permaxrep  45995  fourierdlem31  47147