Theorem nfbi 1936

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

This proof depends on syntax axioms:   ↔ wb 209  ⊤wtru 1571  Ⅎwnf 1816

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

This proof depends on definitions:  df-bi 210  df-an 402  df-or 862  df-tru 1573  df-ex 1813  df-nf 1817

This theorem is used by:  sbbib  2390  euf  2601  sb8eulem  2623  axextmo  2736  abbib  2829  cleqh  2889  cleqf  2950  ceqsexg  3607  elabgf  3628  axrep1  5233  axrep3  5236  axrep4OLD  5239  copsex2t  5469  opeliunxp2  5818  ralxpf  5826  cbviotaw  6496  cbviota  6498  sb8iota  6500  fvopab5  7021  fmptco  7124  nfiso  7324  dfoprab4f  8054  opeliunxp2f  8209  xpf1o  9138  zfcndrep  10624  gsumcom2  20103  isfildlem  24084  cnextfvval  24292  mbfsup  25893  mbfinf  25894  brabgaf  33080  fmptcof2  33131  esplyfval1  34084  bnj1468  35356  subtr2  36935  bj-axseprep  37820  bj-axreprepsep  37821  mpobi123f  38911  eqrelf  39007  unielss  44060  permaxrep  45830  fourierdlem31  46967