Theorem nfbi 1900

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

Syntax hints:   ↔ wb 208  ⊤wtru 1534  Ⅎwnf 1780

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

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

This theorem is referenced by:  sbbibOLD  2285  sbbib  2376  euf  2657  sb8eulem  2680  axextmo  2797  abbi  2888  cleqh  2936  cleqf  3010  sbhypf  3552  ceqsexg  3645  elabgt  3662  elabgf  3663  elabg  3665  axrep1  5183  axrep3  5186  axrep4  5187  copsex2t  5375  copsex2g  5376  opelopabsb  5409  opeliunxp2  5703  ralxpf  5711  cbviotaw  6315  cbviota  6317  sb8iota  6319  fvopab5  6794  fmptco  6885  nfiso  7069  dfoprab4f  7748  opeliunxp2f  7870  xpf1o  8673  zfcndrep  10030  gsumcom2  19089  isfildlem  22459  cnextfvval  22667  mbfsup  24259  mbfinf  24260  brabgaf  30353  fmptcof2  30396  bnj1468  32113  subtr2  33658  mpobi123f  35434  eqrelf  35511  fourierdlem31  42417  dfich2OLD  43610