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 849  df-tru 1543  df-ex 1780  df-nf 1784

This theorem is referenced by:  sbbib  2364  euf  2576  sb8eulem  2598  axextmo  2712  abbib  2811  cleqh  2871  cleqf  2934  sbhypfOLD  3545  ceqsexg  3653  elabgf  3674  axrep1  5280  axrep3  5283  axrep4OLD  5286  copsex2t  5497  opeliunxp2  5849  ralxpf  5857  cbviotaw  6521  cbviota  6523  sb8iota  6525  fvopab5  7049  fmptco  7149  nfiso  7342  dfoprab4f  8081  opeliunxp2f  8235  xpf1o  9179  zfcndrep  10654  gsumcom2  19993  isfildlem  23865  cnextfvval  24073  mbfsup  25699  mbfinf  25700  brabgaf  32620  fmptcof2  32667  bnj1468  34860  subtr2  36316  mpobi123f  38169  eqrelf  38256  unielss  43230  fourierdlem31  46153