Theorem nfbi 1905

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

Syntax hints:   ↔ wb 206  ⊤wtru 1543  Ⅎwnf 1785

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

This theorem depends on definitions:  df-bi 207  df-an 396  df-or 849  df-tru 1545  df-ex 1782  df-nf 1786

This theorem is referenced by:  sbbib  2365  euf  2576  sb8eulem  2598  axextmo  2712  abbib  2805  cleqh  2865  cleqf  2927  ceqsexg  3595  elabgf  3617  axrep1  5213  axrep3  5216  axrep4OLD  5219  copsex2t  5446  opeliunxp2  5793  ralxpf  5801  cbviotaw  6461  cbviota  6463  sb8iota  6465  fvopab5  6981  fmptco  7082  nfiso  7277  dfoprab4f  8009  opeliunxp2f  8160  xpf1o  9077  zfcndrep  10537  gsumcom2  19950  isfildlem  23822  cnextfvval  24030  mbfsup  25631  mbfinf  25632  brabgaf  32679  fmptcof2  32730  esplyfval1  33717  bnj1468  34988  subtr2  36497  bj-axseprep  37381  bj-axreprepsep  37382  mpobi123f  38483  eqrelf  38579  unielss  43646  permaxrep  45433  fourierdlem31  46566