Theorem nfbi 1909

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

Syntax hints:   ↔ wb 209  ⊤wtru 1543  Ⅎwnf 1790

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

This theorem depends on definitions:  df-bi 210  df-an 400  df-or 847  df-tru 1545  df-ex 1787  df-nf 1791

This theorem is referenced by:  sbbib  2361  euf  2577  sb8eulem  2599  axextmo  2714  abbi  2805  cleqh  2856  cleqf  2930  sbhypf  3455  ceqsexg  3547  elabgt  3565  elabgf  3566  elabg  3570  axrep1  5152  axrep3  5155  axrep4  5156  copsex2t  5346  copsex2gOLD  5348  opeliunxp2  5675  ralxpf  5683  cbviotaw  6298  cbviota  6301  sb8iota  6303  fvopab5  6801  fmptco  6895  nfiso  7082  dfoprab4f  7772  opeliunxp2f  7898  xpf1o  8722  zfcndrep  10107  gsumcom2  19207  isfildlem  22601  cnextfvval  22809  mbfsup  24409  mbfinf  24410  brabgaf  30514  fmptcof2  30561  bnj1468  32389  subtr2  34134  mpobi123f  35932  eqrelf  36007  fourierdlem31  43205