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  2360  euf  2570  sb8eulem  2592  axextmo  2706  abbib  2799  cleqh  2858  cleqf  2921  sbhypfOLD  3514  ceqsexg  3622  elabgf  3644  axrep1  5238  axrep3  5241  axrep4OLD  5244  copsex2t  5455  opeliunxp2  5805  ralxpf  5813  cbviotaw  6474  cbviota  6476  sb8iota  6478  fvopab5  7004  fmptco  7104  nfiso  7300  dfoprab4f  8038  opeliunxp2f  8192  xpf1o  9109  zfcndrep  10574  gsumcom2  19912  isfildlem  23751  cnextfvval  23959  mbfsup  25572  mbfinf  25573  brabgaf  32543  fmptcof2  32588  bnj1468  34843  subtr2  36310  mpobi123f  38163  eqrelf  38251  unielss  43214  permaxrep  45003  fourierdlem31  46143