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  2365  euf  2576  sb8eulem  2598  axextmo  2712  abbib  2805  cleqh  2865  cleqf  2927  ceqsexg  3607  elabgf  3629  axrep1  5225  axrep3  5228  axrep4OLD  5231  copsex2t  5440  opeliunxp2  5787  ralxpf  5795  cbviotaw  6455  cbviota  6457  sb8iota  6459  fvopab5  6974  fmptco  7074  nfiso  7268  dfoprab4f  8000  opeliunxp2f  8152  xpf1o  9067  zfcndrep  10525  gsumcom2  19904  isfildlem  23801  cnextfvval  24009  mbfsup  25621  mbfinf  25622  brabgaf  32684  fmptcof2  32735  bnj1468  35002  subtr2  36509  mpobi123f  38363  eqrelf  38453  unielss  43470  permaxrep  45257  fourierdlem31  46392