Theorem nfbi 1903

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

Syntax hints:   ↔ wb 206  ⊤wtru 1541  Ⅎwnf 1783

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

This theorem depends on definitions:  df-bi 207  df-an 396  df-or 848  df-tru 1543  df-ex 1780  df-nf 1784

This theorem is referenced by:  sbbib  2359  euf  2569  sb8eulem  2591  axextmo  2705  abbib  2798  cleqh  2857  cleqf  2920  sbhypfOLD  3500  ceqsexg  3608  elabgf  3630  axrep1  5219  axrep3  5222  axrep4OLD  5225  copsex2t  5435  opeliunxp2  5781  ralxpf  5789  cbviotaw  6445  cbviota  6447  sb8iota  6449  fvopab5  6963  fmptco  7063  nfiso  7259  dfoprab4f  7991  opeliunxp2f  8143  xpf1o  9056  zfcndrep  10508  gsumcom2  19854  isfildlem  23742  cnextfvval  23950  mbfsup  25563  mbfinf  25564  brabgaf  32553  fmptcof2  32600  bnj1468  34813  subtr2  36293  mpobi123f  38146  eqrelf  38234  unielss  43195  permaxrep  44984  fourierdlem31  46123