stdcn - Intuitionistic Logic Explorer

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

Theorem stdcn 848

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

**Assertion**
Ref	Expression
stdcn	STAB DECID DECID

**Proof of Theorem stdcn**
Step	Hyp	Ref	Expression
1		stdcndc 846	. . . 4 STAB $/\$ DECID DECID
2	1	biimpi 120	. . 3 STAB $/\$ DECID DECID
3	2	ex 115	. 2 STAB DECID DECID
4		olc 712	. . . . 5 $\/$
5	4	imim1i 60	. . . 4 $\/$ $\/$ $\/$
6		orel2 727	. . . 4 $\/$
7	5, 6	sylcom 28	. . 3 $\/$ $\/$
8		df-dc 836	. . . 4 DECID $\/$
9		df-dc 836	. . . 4 DECID $\/$
10	8, 9	imbi12i 239	. . 3 DECID DECID $\/$ $\/$
11		df-stab 832	. . 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 709 STAB wstab 831 DECID wdc 835

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 615 ax-in2 616 ax-io 710

This theorem depends on definitions: df-bi 117 df-stab 832 df-dc 836

This theorem is referenced by: dcnn 849 bj-charfunbi 15467

W3C validator