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  2366  euf  2577  sb8eulem  2599  axextmo  2713  abbib  2806  cleqh  2866  cleqf  2928  ceqsexg  3609  elabgf  3631  axrep1  5227  axrep3  5230  axrep4OLD  5233  copsex2t  5448  opeliunxp2  5795  ralxpf  5803  cbviotaw  6463  cbviota  6465  sb8iota  6467  fvopab5  6983  fmptco  7084  nfiso  7278  dfoprab4f  8010  opeliunxp2f  8162  xpf1o  9079  zfcndrep  10537  gsumcom2  19916  isfildlem  23813  cnextfvval  24021  mbfsup  25633  mbfinf  25634  brabgaf  32696  fmptcof2  32747  esplyfval1  33750  bnj1468  35022  subtr2  36531  bj-axseprep  37322  bj-axreprepsep  37323  mpobi123f  38413  eqrelf  38509  unielss  43575  permaxrep  45362  fourierdlem31  46496