Theorem nfbi 1970

Description: If 𝑥 is not free in 𝜑 and 𝜓, 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 1969	. 2 ⊢ (⊤ → Ⅎ𝑥(𝜑 ↔ 𝜓))
6	5	trud 1630	1 ⊢ Ⅎ𝑥(𝜑 ↔ 𝜓)

Syntax hints:   ↔ wb 196  ⊤wtru 1621  Ⅎwnf 1845

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

This theorem depends on definitions:  df-bi 197  df-or 384  df-an 385  df-tru 1623  df-ex 1842  df-nf 1847

This theorem is referenced by:  euf  2603  sb8eu  2629  bm1.1  2733  cleqh  2850  sbhypf  3381  ceqsexg  3461  elabgt  3475  elabgf  3476  axrep1  4912  axrep3  4914  axrep4  4915  copsex2t  5093  copsex2g  5094  opelopabsb  5123  opeliunxp2  5404  ralxpf  5412  cbviota  6005  sb8iota  6007  fvopab5  6460  fmptco  6547  nfiso  6723  dfoprab4f  7381  opeliunxp2f  7493  xpf1o  8275  zfcndrep  9599  gsumcom2  18545  isfildlem  21833  cnextfvval  22041  mbfsup  23601  mbfinf  23602  brabgaf  29698  fmptcof2  29737  bnj1468  31194  subtr2  32586  bj-abbi  33052  bj-axrep1  33065  bj-axrep3  33067  bj-axrep4  33068  mpt2bi123f  34253  eqrelf  34313  fourierdlem31  40827