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  2363  euf  2575  sb8eulem  2597  axextmo  2711  abbib  2804  cleqh  2864  cleqf  2927  sbhypfOLD  3524  ceqsexg  3632  elabgf  3653  axrep1  5250  axrep3  5253  axrep4OLD  5256  copsex2t  5467  opeliunxp2  5818  ralxpf  5826  cbviotaw  6490  cbviota  6492  sb8iota  6494  fvopab5  7018  fmptco  7118  nfiso  7314  dfoprab4f  8053  opeliunxp2f  8207  xpf1o  9151  zfcndrep  10626  gsumcom2  19954  isfildlem  23793  cnextfvval  24001  mbfsup  25615  mbfinf  25616  brabgaf  32534  fmptcof2  32581  bnj1468  34823  subtr2  36279  mpobi123f  38132  eqrelf  38219  unielss  43189  permaxrep  44979  fourierdlem31  46115