Theorem nfbi 1935

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

This proof depends on syntax axioms:   ↔ wb 209  ⊤wtru 1570  Ⅎwnf 1815

This proof depends on axioms:  ax-mp 5  ax-1 6  ax-2 7  ax-3 8  ax-gen 1827  ax-4 1841

This proof depends on definitions:  df-bi 210  df-an 402  df-or 862  df-tru 1572  df-ex 1812  df-nf 1816

This theorem is used by:  sbbib  2390  euf  2601  sb8eulem  2623  axextmo  2736  abbib  2829  cleqh  2889  cleqf  2950  ceqsexg  3606  elabgf  3627  axrep1  5232  axrep3  5235  copsex2t  5464  opeliunxp2  5816  ralxpf  5825  cbviotaw  6504  cbviota  6506  sb8iota  6508  fvopab5  7032  fmptco  7135  nfiso  7334  dfoprab4f  8072  opeliunxp2f  8235  xpf1o  9166  zfcndrep  10706  gsumcom2  20198  isfildlem  24185  cnextfvval  24393  mbfsup  25994  mbfinf  25995  brabgaf  33251  fmptcof2  33302  esplyfval1  34255  bnj1468  35526  subtr2  37227  bj-axseprep  38126  bj-axreprepsep  38127  mpobi123f  39231  eqrelf  39327  unielss  44357  permaxrep  46132  fourierdlem31  47284