Theorem nfbi 2003

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

Syntax hints:   ↔ wb 198  ⊤wtru 1654  Ⅎwnf 1879

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

This theorem depends on definitions:  df-bi 199  df-an 386  df-or 875  df-tru 1657  df-ex 1876  df-nf 1880

This theorem is referenced by:  euf  2615  eufOLD  2616  sb8eu  2652  axextmo  2782  bm1.1OLD  2783  cleqh  2901  sbhypf  3441  ceqsexg  3523  elabgt  3537  elabgf  3538  elabg  3540  axrep1  4965  axrep3  4968  axrep4  4969  copsex2t  5147  copsex2g  5148  opelopabsb  5181  opeliunxp2  5464  ralxpf  5472  cbviota  6069  sb8iota  6071  fvopab5  6535  fmptco  6623  nfiso  6800  dfoprab4f  7461  opeliunxp2f  7574  xpf1o  8364  zfcndrep  9724  gsumcom2  18689  isfildlem  21989  cnextfvval  22197  mbfsup  23772  mbfinf  23773  brabgaf  29937  fmptcof2  29976  bnj1468  31433  subtr2  32822  bj-abbi  33271  bj-axrep1  33284  bj-axrep3  33286  bj-axrep4  33287  mpt2bi123f  34457  eqrelf  34520  fourierdlem31  41098