Theorem nfbi 1906

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

Syntax hints:   ↔ wb 205  ⊤wtru 1540  Ⅎwnf 1786

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

This theorem depends on definitions:  df-bi 206  df-an 397  df-or 845  df-tru 1542  df-ex 1783  df-nf 1787

This theorem is referenced by:  sbbib  2359  euf  2576  sb8eulem  2598  axextmo  2713  abbi  2810  cleqh  2862  cleqf  2938  sbhypf  3491  ceqsexg  3583  elabgtOLD  3604  elabgf  3605  elabgOLD  3608  axrep1  5210  axrep3  5213  axrep4  5214  copsex2t  5406  copsex2gOLD  5408  opeliunxp2  5747  ralxpf  5755  cbviotaw  6398  cbviota  6401  sb8iota  6403  fvopab5  6907  fmptco  7001  nfiso  7193  dfoprab4f  7896  opeliunxp2f  8026  xpf1o  8926  zfcndrep  10370  gsumcom2  19576  isfildlem  23008  cnextfvval  23216  mbfsup  24828  mbfinf  24829  brabgaf  30948  fmptcof2  30994  bnj1468  32826  subtr2  34504  mpobi123f  36320  eqrelf  36395  fourierdlem31  43679