Theorem nfbi 1904

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

Syntax hints:   ↔ wb 208  ⊤wtru 1538  Ⅎwnf 1784

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

This theorem depends on definitions:  df-bi 209  df-an 399  df-or 844  df-tru 1540  df-ex 1781  df-nf 1785

This theorem is referenced by:  sbbibOLD  2289  sbbib  2380  euf  2661  sb8eulem  2684  axextmo  2799  abbi  2890  cleqh  2938  cleqf  3012  sbhypf  3554  ceqsexg  3648  elabgt  3665  elabgf  3666  elabg  3668  axrep1  5193  axrep3  5196  axrep4  5197  copsex2t  5385  copsex2g  5386  opelopabsb  5419  opeliunxp2  5711  ralxpf  5719  cbviotaw  6323  cbviota  6325  sb8iota  6327  fvopab5  6802  fmptco  6893  nfiso  7077  dfoprab4f  7756  opeliunxp2f  7878  xpf1o  8681  zfcndrep  10038  gsumcom2  19097  isfildlem  22467  cnextfvval  22675  mbfsup  24267  mbfinf  24268  brabgaf  30361  fmptcof2  30404  bnj1468  32120  subtr2  33665  mpobi123f  35442  eqrelf  35519  fourierdlem31  42430  dfich2OLD  43623