Theorem nfbi 1904

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

Syntax hints:   ↔ wb 209  ⊤wtru 1539  Ⅎ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 210  df-an 400  df-or 845  df-tru 1541  df-ex 1782  df-nf 1786

This theorem is referenced by:  sbbibOLD  2285  sbbib  2369  euf  2636  sb8eulem  2659  axextmo  2774  abbi  2865  cleqh  2913  cleqf  2983  sbhypf  3500  ceqsexg  3594  elabgt  3609  elabgf  3610  elabg  3614  axrep1  5155  axrep3  5158  axrep4  5159  copsex2t  5348  copsex2g  5349  opelopabsb  5382  opeliunxp2  5673  ralxpf  5681  cbviotaw  6290  cbviota  6292  sb8iota  6294  fvopab5  6777  fmptco  6868  nfiso  7054  dfoprab4f  7736  opeliunxp2f  7859  xpf1o  8663  zfcndrep  10025  gsumcom2  19088  isfildlem  22462  cnextfvval  22670  mbfsup  24268  mbfinf  24269  brabgaf  30372  fmptcof2  30420  bnj1468  32228  subtr2  33776  mpobi123f  35600  eqrelf  35677  fourierdlem31  42780