stdcn - Intuitionistic Logic Explorer

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

Theorem stdcn 832

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 827. (Contributed by BJ, 18-Nov-2023.)

**Assertion**
Ref	Expression
stdcn	STAB DECID DECID

**Proof of Theorem stdcn**
Step	Hyp	Ref	Expression
1		stdcndc 830	. . . 4 STAB $/\$ DECID DECID
2	1	biimpi 119	. . 3 STAB $/\$ DECID DECID
3	2	ex 114	. 2 STAB DECID DECID
4		olc 700	. . . . 5 $\/$
5	4	imim1i 60	. . . 4 $\/$ $\/$ $\/$
6		orel2 715	. . . 4 $\/$
7	5, 6	sylcom 28	. . 3 $\/$ $\/$
8		df-dc 820	. . . 4 DECID $\/$
9		df-dc 820	. . . 4 DECID $\/$
10	8, 9	imbi12i 238	. . 3 DECID DECID $\/$ $\/$
11		df-stab 816	. . 3 STAB
12	7, 10, 11	3imtr4i 200	. 2 DECID DECID STAB
13	3, 12	impbii 125	1 STAB DECID DECID

Colors of variables: wff set class

Syntax hints:

wn 3

wi 4 $/\$ wa 103

wb 104 $\/$ wo 697 STAB wstab 815 DECID wdc 819

This theorem was proved from axioms: ax-mp 5 ax-1 6 ax-2 7 ax-ia1 105 ax-ia2 106 ax-ia3 107 ax-in1 603 ax-in2 604 ax-io 698

This theorem depends on definitions: df-bi 116 df-stab 816 df-dc 820

This theorem is referenced by: dcnn 833

W3C validator