Theorem nfbi 1902

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

Syntax hints:   ↔ wb 206  ⊤wtru 1538  Ⅎwnf 1781

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

This theorem depends on definitions:  df-bi 207  df-an 396  df-or 847  df-tru 1540  df-ex 1778  df-nf 1782

This theorem is referenced by:  sbbib  2367  euf  2579  sb8eulem  2601  axextmo  2715  abbib  2814  cleqh  2874  cleqf  2940  sbhypfOLD  3557  ceqsexg  3666  elabgtOLDOLD  3687  elabgf  3688  elabgOLD  3691  axrep1  5304  axrep3  5307  axrep4  5308  copsex2t  5512  opeliunxp2  5863  ralxpf  5871  cbviotaw  6532  cbviota  6535  sb8iota  6537  fvopab5  7062  fmptco  7163  nfiso  7358  dfoprab4f  8097  opeliunxp2f  8251  xpf1o  9205  zfcndrep  10683  gsumcom2  20017  isfildlem  23886  cnextfvval  24094  mbfsup  25718  mbfinf  25719  brabgaf  32630  fmptcof2  32675  bnj1468  34822  subtr2  36281  mpobi123f  38122  eqrelf  38211  unielss  43179  fourierdlem31  46059