Theorem nfbi 1899

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

Syntax hints:   ↔ wb 205  ⊤wtru 1535  Ⅎwnf 1778

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

This theorem depends on definitions:  df-bi 206  df-an 396  df-or 847  df-tru 1537  df-ex 1775  df-nf 1779

This theorem is referenced by:  sbbib  2352  euf  2565  sb8eulem  2587  axextmo  2702  abbib  2799  cleqh  2858  cleqf  2929  sbhypfOLD  3535  ceqsexg  3637  elabgtOLDOLD  3660  elabgf  3661  elabgOLD  3664  axrep1  5280  axrep3  5283  axrep4  5284  copsex2t  5488  copsex2gOLD  5490  opeliunxp2  5835  ralxpf  5843  cbviotaw  6501  cbviota  6504  sb8iota  6506  fvopab5  7032  fmptco  7132  nfiso  7324  dfoprab4f  8054  opeliunxp2f  8209  xpf1o  9155  zfcndrep  10629  gsumcom2  19921  isfildlem  23748  cnextfvval  23956  mbfsup  25580  mbfinf  25581  brabgaf  32381  fmptcof2  32426  bnj1468  34413  subtr2  35735  mpobi123f  37570  eqrelf  37662  unielss  42569  fourierdlem31  45449