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 1548	1 ⊢ Ⅎ𝑥(𝜑 ↔ 𝜓)

Syntax hints:   ↔ wb 206  ⊤wtru 1542  Ⅎwnf 1784

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

This theorem depends on definitions:  df-bi 207  df-an 396  df-or 848  df-tru 1544  df-ex 1781  df-nf 1785

This theorem is referenced by:  sbbib  2363  euf  2574  sb8eulem  2596  axextmo  2710  abbib  2803  cleqh  2863  cleqf  2925  ceqsexg  3605  elabgf  3627  axrep1  5223  axrep3  5226  axrep4OLD  5229  copsex2t  5438  opeliunxp2  5785  ralxpf  5793  cbviotaw  6453  cbviota  6455  sb8iota  6457  fvopab5  6972  fmptco  7072  nfiso  7266  dfoprab4f  7998  opeliunxp2f  8150  xpf1o  9065  zfcndrep  10523  gsumcom2  19902  isfildlem  23799  cnextfvval  24007  mbfsup  25619  mbfinf  25620  brabgaf  32633  fmptcof2  32684  bnj1468  34951  subtr2  36458  mpobi123f  38302  eqrelf  38392  unielss  43402  permaxrep  45189  fourierdlem31  46324