dn1dc - Intuitionistic Logic Explorer

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

Theorem dn1dc 960

Description: DN₁ for decidable propositions. Without the decidability conditions, DN₁ can serve as a single axiom for Boolean algebra. See http://www-unix.mcs.anl.gov/~mccune/papers/basax/v12.pdf. (Contributed by Jim Kingdon, 22-Apr-2018.)

**Assertion**
Ref	Expression
dn1dc	DECID $/\$ DECID $/\$ DECID $/\$ DECID $\/$ $\/$ $\/$ $\/$ $\/$ $\/$

**Proof of Theorem dn1dc**
Step	Hyp	Ref	Expression
1		pm2.45 738	. . . . 5 $\/$
2		imnan 690	. . . . 5 $\/$ $\/$ $/\$
3	1, 2	mpbi 145	. . . 4 $\/$ $/\$
4	3	biorfi 746	. . 3 $\/$ $\/$ $/\$
5		orcom 728	. . 3 $\/$ $\/$ $/\$ $\/$ $/\$ $\/$
6		ordir 817	. . 3 $\/$ $/\$ $\/$ $\/$ $\/$ $/\$ $\/$
7	4, 5, 6	3bitri 206	. 2 $\/$ $\/$ $/\$ $\/$
8		pm4.45 784	. . . . . 6 $/\$ $\/$
9		simprrl 539	. . . . . . 7 DECID $/\$ DECID $/\$ DECID $/\$ DECID DECID
10		dcor 935	. . . . . . . . 9 DECID DECID DECID $\/$
11	10	imp 124	. . . . . . . 8 DECID $/\$ DECID DECID $\/$
12	11	ad2antll 491	. . . . . . 7 DECID $/\$ DECID $/\$ DECID $/\$ DECID DECID $\/$
13		anordc 956	. . . . . . 7 DECID DECID $\/$ $/\$ $\/$ $\/$ $\/$
14	9, 12, 13	sylc 62	. . . . . 6 DECID $/\$ DECID $/\$ DECID $/\$ DECID $/\$ $\/$ $\/$ $\/$
15	8, 14	bitrid 192	. . . . 5 DECID $/\$ DECID $/\$ DECID $/\$ DECID $\/$ $\/$
16	15	orbi2d 790	. . . 4 DECID $/\$ DECID $/\$ DECID $/\$ DECID $\/$ $\/$ $\/$ $\/$
17	16	anbi2d 464	. . 3 DECID $/\$ DECID $/\$ DECID $/\$ DECID $\/$ $\/$ $/\$ $\/$ $\/$ $\/$ $/\$ $\/$ $\/$ $\/$
18		dcor 935	. . . . . . . 8 DECID DECID DECID $\/$
19		dcn 842	. . . . . . . 8 DECID $\/$ DECID $\/$
20	18, 19	syl6 33	. . . . . . 7 DECID DECID DECID $\/$
21	20	imp 124	. . . . . 6 DECID $/\$ DECID DECID $\/$
22	21	adantrr 479	. . . . 5 DECID $/\$ DECID $/\$ DECID $/\$ DECID DECID $\/$
23		dcor 935	. . . . 5 DECID $\/$ DECID DECID $\/$ $\/$
24	22, 9, 23	sylc 62	. . . 4 DECID $/\$ DECID $/\$ DECID $/\$ DECID DECID $\/$ $\/$
25		dcn 842	. . . . . . . 8 DECID DECID
26	9, 25	syl 14	. . . . . . 7 DECID $/\$ DECID $/\$ DECID $/\$ DECID DECID
27		dcn 842	. . . . . . . 8 DECID $\/$ DECID $\/$
28	12, 27	syl 14	. . . . . . 7 DECID $/\$ DECID $/\$ DECID $/\$ DECID DECID $\/$
29		dcor 935	. . . . . . 7 DECID DECID $\/$ DECID $\/$ $\/$
30	26, 28, 29	sylc 62	. . . . . 6 DECID $/\$ DECID $/\$ DECID $/\$ DECID DECID $\/$ $\/$
31		dcn 842	. . . . . 6 DECID $\/$ $\/$ DECID $\/$ $\/$
32	30, 31	syl 14	. . . . 5 DECID $/\$ DECID $/\$ DECID $/\$ DECID DECID $\/$ $\/$
33		dcor 935	. . . . . 6 DECID DECID $\/$ $\/$ DECID $\/$ $\/$ $\/$
34	33	imp 124	. . . . 5 DECID $/\$ DECID $\/$ $\/$ DECID $\/$ $\/$ $\/$
35	32, 34	syldan 282	. . . 4 DECID $/\$ DECID $/\$ DECID $/\$ DECID DECID $\/$ $\/$ $\/$
36		anordc 956	. . . 4 DECID $\/$ $\/$ DECID $\/$ $\/$ $\/$ $\/$ $\/$ $/\$ $\/$ $\/$ $\/$ $\/$ $\/$ $\/$ $\/$ $\/$ $\/$
37	24, 35, 36	sylc 62	. . 3 DECID $/\$ DECID $/\$ DECID $/\$ DECID $\/$ $\/$ $/\$ $\/$ $\/$ $\/$ $\/$ $\/$ $\/$ $\/$ $\/$ $\/$
38	17, 37	bitrd 188	. 2 DECID $/\$ DECID $/\$ DECID $/\$ DECID $\/$ $\/$ $/\$ $\/$ $\/$ $\/$ $\/$ $\/$ $\/$ $\/$
39	7, 38	bitr2id 193	1 DECID $/\$ DECID $/\$ DECID $/\$ DECID $\/$ $\/$ $\/$ $\/$ $\/$ $\/$

Colors of variables: wff set class

Syntax hints:

wn 3

wi 4 $/\$ wa 104

wb 105 $\/$ wo 708 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: (None)

W3C validator