Theorem nfbi 1900

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

Syntax hints:   ↔ wb 206  ⊤wtru 1537  Ⅎwnf 1779

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

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

This theorem is referenced by:  sbbib  2361  euf  2573  sb8eulem  2595  axextmo  2709  abbib  2808  cleqh  2868  cleqf  2931  sbhypfOLD  3544  ceqsexg  3652  elabgtOLDOLD  3673  elabgf  3674  elabgOLD  3677  axrep1  5285  axrep3  5288  axrep4OLD  5291  copsex2t  5502  opeliunxp2  5851  ralxpf  5859  cbviotaw  6522  cbviota  6524  sb8iota  6526  fvopab5  7048  fmptco  7148  nfiso  7341  dfoprab4f  8079  opeliunxp2f  8233  xpf1o  9177  zfcndrep  10651  gsumcom2  20007  isfildlem  23880  cnextfvval  24088  mbfsup  25712  mbfinf  25713  brabgaf  32627  fmptcof2  32673  bnj1468  34838  subtr2  36297  mpobi123f  38148  eqrelf  38236  unielss  43206  fourierdlem31  46093