Theorem nfbi 1910

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

Syntax hints:   ↔ wb 207  ⊤wtru 1548  Ⅎwnf 1790

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

This theorem depends on definitions:  df-bi 208  df-an 397  df-or 854  df-tru 1550  df-ex 1787  df-nf 1791

This theorem is referenced by:  sbbib  2369  euf  2580  sb8eulem  2602  axextmo  2715  abbib  2808  cleqh  2868  cleqf  2929  ceqsexg  3591  elabgf  3612  axrep1  5200  axrep3  5203  axrep4OLD  5206  copsex2t  5433  opeliunxp2  5780  ralxpf  5788  cbviotaw  6448  cbviota  6450  sb8iota  6452  fvopab5  6969  fmptco  7071  nfiso  7266  dfoprab4f  7998  opeliunxp2f  8150  xpf1o  9067  zfcndrep  10528  gsumcom2  19941  isfildlem  23840  cnextfvval  24048  mbfsup  25649  mbfinf  25650  brabgaf  32698  fmptcof2  32749  esplyfval1  33757  bnj1468  35028  subtr2  36543  bj-axseprep  37427  bj-axreprepsep  37428  mpobi123f  38529  eqrelf  38625  unielss  43663  permaxrep  45450  fourierdlem31  46581