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  2395  euf  2606  sb8eulem  2628  axextmo  2741  abbib  2834  cleqh  2894  cleqf  2955  ceqsexg  3614  elabgf  3635  axrep1  5241  axrep3  5244  axrep4OLD  5247  copsex2t  5477  opeliunxp2  5826  ralxpf  5834  cbviotaw  6503  cbviota  6505  sb8iota  6507  fvopab5  7027  fmptco  7129  nfiso  7329  dfoprab4f  8059  opeliunxp2f  8212  xpf1o  9134  zfcndrep  10616  gsumcom2  20091  isfildlem  24067  cnextfvval  24275  mbfsup  25876  mbfinf  25877  brabgaf  33024  fmptcof2  33075  esplyfval1  34029  bnj1468  35301  subtr2  36885  bj-axseprep  37770  bj-axreprepsep  37771  mpobi123f  38871  eqrelf  38967  unielss  44005  permaxrep  45775  fourierdlem31  46912