stdcn - Intuitionistic Logic Explorer

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

Theorem stdcn 842

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

**Assertion**
Ref	Expression
stdcn	STAB DECID DECID

**Proof of Theorem stdcn**
Step	Hyp	Ref	Expression
1		stdcndc 840	. . . 4 STAB $/\$ DECID DECID
2	1	biimpi 119	. . 3 STAB $/\$ DECID DECID
3	2	ex 114	. 2 STAB DECID DECID
4		olc 706	. . . . 5 $\/$
5	4	imim1i 60	. . . 4 $\/$ $\/$ $\/$
6		orel2 721	. . . 4 $\/$
7	5, 6	sylcom 28	. . 3 $\/$ $\/$
8		df-dc 830	. . . 4 DECID $\/$
9		df-dc 830	. . . 4 DECID $\/$
10	8, 9	imbi12i 238	. . 3 DECID DECID $\/$ $\/$
11		df-stab 826	. . 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 703 STAB wstab 825 DECID wdc 829

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 609 ax-in2 610 ax-io 704

This theorem depends on definitions: df-bi 116 df-stab 826 df-dc 830

This theorem is referenced by: dcnn 843 bj-charfunbi 13846

W3C validator