Theorem nfbi 1907

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

Syntax hints:   ↔ wb 205  ⊤wtru 1540  Ⅎwnf 1787

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

This theorem depends on definitions:  df-bi 206  df-an 396  df-or 844  df-tru 1542  df-ex 1784  df-nf 1788

This theorem is referenced by:  sbbib  2359  euf  2576  sb8eulem  2598  axextmo  2713  abbi  2811  cleqh  2862  cleqf  2937  sbhypf  3481  ceqsexg  3575  elabgtOLD  3597  elabgf  3598  elabgOLD  3601  axrep1  5206  axrep3  5209  axrep4  5210  copsex2t  5400  copsex2gOLD  5402  opeliunxp2  5736  ralxpf  5744  cbviotaw  6383  cbviota  6386  sb8iota  6388  fvopab5  6889  fmptco  6983  nfiso  7173  dfoprab4f  7869  opeliunxp2f  7997  xpf1o  8875  zfcndrep  10301  gsumcom2  19491  isfildlem  22916  cnextfvval  23124  mbfsup  24733  mbfinf  24734  brabgaf  30849  fmptcof2  30896  bnj1468  32726  subtr2  34431  mpobi123f  36247  eqrelf  36322  fourierdlem31  43569