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  3508  ceqsexg  3616  elabgf  3638  axrep1  5230  axrep3  5233  axrep4OLD  5236  copsex2t  5447  opeliunxp2  5792  ralxpf  5800  cbviotaw  6459  cbviota  6461  sb8iota  6463  fvopab5  6983  fmptco  7083  nfiso  7279  dfoprab4f  8014  opeliunxp2f  8166  xpf1o  9080  zfcndrep  10543  gsumcom2  19889  isfildlem  23777  cnextfvval  23985  mbfsup  25598  mbfinf  25599  brabgaf  32586  fmptcof2  32631  bnj1468  34829  subtr2  36296  mpobi123f  38149  eqrelf  38237  unielss  43200  permaxrep  44989  fourierdlem31  46129