Theorem nfbi 1907

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

Syntax hints:   ↔ wb 205  ⊤wtru 1543  Ⅎwnf 1786

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

This theorem depends on definitions:  df-bi 206  df-an 398  df-or 847  df-tru 1545  df-ex 1783  df-nf 1787

This theorem is referenced by:  sbbib  2358  euf  2571  sb8eulem  2593  axextmo  2708  abbib  2805  cleqh  2864  cleqf  2935  sbhypfOLD  3540  ceqsexg  3642  elabgtOLD  3664  elabgf  3665  elabgOLD  3668  axrep1  5287  axrep3  5290  axrep4  5291  copsex2t  5493  copsex2gOLD  5495  opeliunxp2  5839  ralxpf  5847  cbviotaw  6503  cbviota  6506  sb8iota  6508  fvopab5  7031  fmptco  7127  nfiso  7319  dfoprab4f  8042  opeliunxp2f  8195  xpf1o  9139  zfcndrep  10609  gsumcom2  19843  isfildlem  23361  cnextfvval  23569  mbfsup  25181  mbfinf  25182  brabgaf  31837  fmptcof2  31882  bnj1468  33857  subtr2  35200  mpobi123f  37030  eqrelf  37123  unielss  41967  fourierdlem31  44854