Theorem nfbi 1938

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 1937	. 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  2393  euf  2604  sb8eulem  2626  axextmo  2739  abbibOLD  2833  cleqh  2893  cleqf  2954  ceqsexg  3610  elabgf  3631  axrep1  5239  axrep3  5242  copsex2t  5471  opeliunxp2  5825  ralxpf  5834  cbviotaw  6527  cbviota  6529  sb8iota  6531  fvopab5  7058  fmptco  7162  nfiso  7361  dfoprab4f  8102  opeliunxp2f  8265  xpf1o  9196  zfcndrep  10738  gsumcom2  20240  isfildlem  24231  cnextfvval  24439  mbfsup  26040  mbfinf  26041  brabgaf  33298  fmptcof2  33349  esplyfval1  34316  bnj1468  35587  subtr2  37318  bj-axseprep  38260  bj-axreprepsep  38261  mpobi123f  39360  eqrelf  39456  unielss  44481  permaxrep  46260  fourierdlem31  47421