Theorem nfbi 1930

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

Syntax hints:   ↔ wb 209  ⊤wtru 1568  Ⅎwnf 1810

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

This theorem depends on definitions:  df-bi 210  df-an 401  df-or 861  df-tru 1570  df-ex 1807  df-nf 1811

This theorem is referenced by:  sbbib  2399  euf  2610  sb8eulem  2632  axextmo  2745  abbib  2838  cleqh  2898  cleqf  2959  ceqsexg  3621  elabgf  3642  axrep1  5243  axrep3  5246  axrep4OLD  5249  copsex2t  5476  opeliunxp2  5825  ralxpf  5833  cbviotaw  6500  cbviota  6502  sb8iota  6504  fvopab5  7024  fmptco  7126  nfiso  7321  dfoprab4f  8053  opeliunxp2f  8206  xpf1o  9127  zfcndrep  10599  gsumcom2  20045  isfildlem  23983  cnextfvval  24191  mbfsup  25792  mbfinf  25793  brabgaf  32892  fmptcof2  32943  esplyfval1  33908  bnj1468  35179  subtr2  36715  bj-axseprep  37599  bj-axreprepsep  37600  mpobi123f  38701  eqrelf  38797  unielss  43837  permaxrep  45607  fourierdlem31  46744