Theorem nfbi 1903

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

Syntax hints:   ↔ wb 206  ⊤wtru 1541  Ⅎwnf 1783

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

This theorem depends on definitions:  df-bi 207  df-an 396  df-or 848  df-tru 1543  df-ex 1780  df-nf 1784

This theorem is referenced by:  sbbib  2359  euf  2569  sb8eulem  2591  axextmo  2705  abbib  2798  cleqh  2857  cleqf  2920  sbhypfOLD  3511  ceqsexg  3619  elabgf  3641  axrep1  5235  axrep3  5238  axrep4OLD  5241  copsex2t  5452  opeliunxp2  5802  ralxpf  5810  cbviotaw  6471  cbviota  6473  sb8iota  6475  fvopab5  7001  fmptco  7101  nfiso  7297  dfoprab4f  8035  opeliunxp2f  8189  xpf1o  9103  zfcndrep  10567  gsumcom2  19905  isfildlem  23744  cnextfvval  23952  mbfsup  25565  mbfinf  25566  brabgaf  32536  fmptcof2  32581  bnj1468  34836  subtr2  36303  mpobi123f  38156  eqrelf  38244  unielss  43207  permaxrep  44996  fourierdlem31  46136