Definition df-stab 838

Description: Propositions where a double-negative can be removed are called stable. See Chapter 2 [Moschovakis] p. 2.

Our notation for stability is a connective STAB which we place before the formula in question. For example, STAB x = y corresponds to " x = y is stable".

(Contributed by David A. Wheeler, 13-Aug-2018.)

Assertion

Ref	Expression
df-stab	|- (STAB ph <-> ( -. -. ph -> ph ) )

Detailed syntax breakdown of Definition df-stab

Step	Hyp	Ref	Expression
1		wph	. . 3 wff ph
2	1	wstab 837	. 2 wff STAB ph
3	1	wn 3	. . . 4 wff -. ph
4	3	wn 3	. . 3 wff -. -. ph
5	4, 1	wi 4	. 2 wff ( -. -. ph -> ph )
6	2, 5	wb 105	1 wff (STAB ph <-> ( -. -. ph -> ph ) )

This definition is referenced by:  stbid  839  stabnot  840  dcstab  851  stdcndc  852  stdcndcOLD  853  stdcn  854  const  859  imanst  895  ddifstab  3339  exmid1stab  4298  2omotap  7478  bj-trst  16386  bj-fast  16388  bj-nnbist  16391  bj-stim  16393  bj-stan  16394  bj-stand  16395  bj-stal  16396  bj-pm2.18st  16397  bj-con1st  16398  bdstab  16473  subctctexmid  16652