Theorem nfbi 1923

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

Syntax hints:   ↔ wb 208  ⊤wtru 1561  Ⅎwnf 1803

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

This theorem depends on definitions:  df-bi 209  df-an 400  df-or 859  df-tru 1563  df-ex 1800  df-nf 1804

This theorem is referenced by:  sbbib  2392  euf  2603  sb8eulem  2625  axextmo  2738  abbib  2831  cleqh  2891  cleqf  2952  ceqsexg  3612  elabgf  3633  axrep1  5228  axrep3  5231  axrep4OLD  5234  copsex2t  5461  opeliunxp2  5810  ralxpf  5818  cbviotaw  6484  cbviota  6486  sb8iota  6488  fvopab5  7009  fmptco  7111  nfiso  7306  dfoprab4f  8037  opeliunxp2f  8190  xpf1o  9111  zfcndrep  10572  gsumcom2  20015  isfildlem  23917  cnextfvval  24125  mbfsup  25726  mbfinf  25727  brabgaf  32808  fmptcof2  32859  esplyfval1  33870  bnj1468  35141  subtr2  36675  bj-axseprep  37559  bj-axreprepsep  37560  mpobi123f  38661  eqrelf  38757  unielss  43795  permaxrep  45582  fourierdlem31  46712