stdcn - Intuitionistic Logic Explorer

	Intuitionistic Logic Explorer		< Previous Next > Nearby theorems
Mirrors > Home > ILE Home > Th. List > stdcn		Unicode version

Theorem stdcn 847

Description: A formula is stable if and only if the decidability of its negation implies its decidability. Note that the right-hand side of this biconditional is the converse of dcn 842. (Contributed by BJ, 18-Nov-2023.)

**Assertion**
Ref	Expression
stdcn	STAB DECID DECID

**Proof of Theorem stdcn**
Step	Hyp	Ref	Expression
1		stdcndc 845	. . . 4 STAB $/\$ DECID DECID
2	1	biimpi 120	. . 3 STAB $/\$ DECID DECID
3	2	ex 115	. 2 STAB DECID DECID
4		olc 711	. . . . 5 $\/$
5	4	imim1i 60	. . . 4 $\/$ $\/$ $\/$
6		orel2 726	. . . 4 $\/$
7	5, 6	sylcom 28	. . 3 $\/$ $\/$
8		df-dc 835	. . . 4 DECID $\/$
9		df-dc 835	. . . 4 DECID $\/$
10	8, 9	imbi12i 239	. . 3 DECID DECID $\/$ $\/$
11		df-stab 831	. . 3 STAB
12	7, 10, 11	3imtr4i 201	. 2 DECID DECID STAB
13	3, 12	impbii 126	1 STAB DECID DECID

Colors of variables: wff set class

Syntax hints:

wn 3

wi 4 $/\$ wa 104

wb 105 $\/$ wo 708 STAB wstab 830 DECID wdc 834

This theorem was proved from axioms: ax-mp 5 ax-1 6 ax-2 7 ax-ia1 106 ax-ia2 107 ax-ia3 108 ax-in1 614 ax-in2 615 ax-io 709

This theorem depends on definitions: df-bi 117 df-stab 831 df-dc 835

This theorem is referenced by: dcnn 848 bj-charfunbi 14648

W3C validator