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  3596  elabgf  3618  axrep1  5214  axrep3  5217  axrep4OLD  5220  copsex2t  5441  opeliunxp2  5788  ralxpf  5796  cbviotaw  6456  cbviota  6458  sb8iota  6460  fvopab5  6976  fmptco  7077  nfiso  7271  dfoprab4f  8003  opeliunxp2f  8154  xpf1o  9071  zfcndrep  10531  gsumcom2  19944  isfildlem  23835  cnextfvval  24043  mbfsup  25644  mbfinf  25645  brabgaf  32697  fmptcof2  32748  esplyfval1  33735  bnj1468  35007  subtr2  36516  bj-axseprep  37400  bj-axreprepsep  37401  mpobi123f  38500  eqrelf  38596  unielss  43667  permaxrep  45454  fourierdlem31  46587