dn1dc - Intuitionistic Logic Explorer

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

Theorem dn1dc 866

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 656	. . . . 5 $\/$
2		imnan 623	. . . . 5 $\/$ $\/$ $/\$
3	1, 2	mpbi 133	. . . 4 $\/$ $/\$
4	3	biorfi 664	. . 3 $\/$ $\/$ $/\$
5		orcom 646	. . 3 $\/$ $\/$ $/\$ $\/$ $/\$ $\/$
6		ordir 729	. . 3 $\/$ $/\$ $\/$ $\/$ $\/$ $/\$ $\/$
7	4, 5, 6	3bitri 195	. 2 $\/$ $\/$ $/\$ $\/$
8		pm4.45 697	. . . . . 6 $/\$ $\/$
9		simprrl 491	. . . . . . 7 DECID $/\$ DECID $/\$ DECID $/\$ DECID DECID
10		dcor 842	. . . . . . . . 9 DECID DECID DECID $\/$
11	10	imp 115	. . . . . . . 8 DECID $/\$ DECID DECID $\/$
12	11	ad2antll 460	. . . . . . 7 DECID $/\$ DECID $/\$ DECID $/\$ DECID DECID $\/$
13		anordc 862	. . . . . . 7 DECID DECID $\/$ $/\$ $\/$ $\/$ $\/$
14	9, 12, 13	sylc 56	. . . . . 6 DECID $/\$ DECID $/\$ DECID $/\$ DECID $/\$ $\/$ $\/$ $\/$
15	8, 14	syl5bb 181	. . . . 5 DECID $/\$ DECID $/\$ DECID $/\$ DECID $\/$ $\/$
16	15	orbi2d 703	. . . 4 DECID $/\$ DECID $/\$ DECID $/\$ DECID $\/$ $\/$ $\/$ $\/$
17	16	anbi2d 437	. . 3 DECID $/\$ DECID $/\$ DECID $/\$ DECID $\/$ $\/$ $/\$ $\/$ $\/$ $\/$ $/\$ $\/$ $\/$ $\/$
18		dcor 842	. . . . . . . 8 DECID DECID DECID $\/$
19		dcn 745	. . . . . . . 8 DECID $\/$ DECID $\/$
20	18, 19	syl6 29	. . . . . . 7 DECID DECID DECID $\/$
21	20	imp 115	. . . . . 6 DECID $/\$ DECID DECID $\/$
22	21	adantrr 448	. . . . 5 DECID $/\$ DECID $/\$ DECID $/\$ DECID DECID $\/$
23		dcor 842	. . . . 5 DECID $\/$ DECID DECID $\/$ $\/$
24	22, 9, 23	sylc 56	. . . 4 DECID $/\$ DECID $/\$ DECID $/\$ DECID DECID $\/$ $\/$
25		dcn 745	. . . . . . . 8 DECID DECID
26	9, 25	syl 14	. . . . . . 7 DECID $/\$ DECID $/\$ DECID $/\$ DECID DECID
27		dcn 745	. . . . . . . 8 DECID $\/$ DECID $\/$
28	12, 27	syl 14	. . . . . . 7 DECID $/\$ DECID $/\$ DECID $/\$ DECID DECID $\/$
29		dcor 842	. . . . . . 7 DECID DECID $\/$ DECID $\/$ $\/$
30	26, 28, 29	sylc 56	. . . . . 6 DECID $/\$ DECID $/\$ DECID $/\$ DECID DECID $\/$ $\/$
31		dcn 745	. . . . . 6 DECID $\/$ $\/$ DECID $\/$ $\/$
32	30, 31	syl 14	. . . . 5 DECID $/\$ DECID $/\$ DECID $/\$ DECID DECID $\/$ $\/$
33		dcor 842	. . . . . 6 DECID DECID $\/$ $\/$ DECID $\/$ $\/$ $\/$
34	33	imp 115	. . . . 5 DECID $/\$ DECID $\/$ $\/$ DECID $\/$ $\/$ $\/$
35	32, 34	syldan 266	. . . 4 DECID $/\$ DECID $/\$ DECID $/\$ DECID DECID $\/$ $\/$ $\/$
36		anordc 862	. . . 4 DECID $\/$ $\/$ DECID $\/$ $\/$ $\/$ $\/$ $\/$ $/\$ $\/$ $\/$ $\/$ $\/$ $\/$ $\/$ $\/$ $\/$ $\/$
37	24, 35, 36	sylc 56	. . 3 DECID $/\$ DECID $/\$ DECID $/\$ DECID $\/$ $\/$ $/\$ $\/$ $\/$ $\/$ $\/$ $\/$ $\/$ $\/$ $\/$ $\/$
38	17, 37	bitrd 177	. 2 DECID $/\$ DECID $/\$ DECID $/\$ DECID $\/$ $\/$ $/\$ $\/$ $\/$ $\/$ $\/$ $\/$ $\/$ $\/$
39	7, 38	syl5rbb 182	1 DECID $/\$ DECID $/\$ DECID $/\$ DECID $\/$ $\/$ $\/$ $\/$ $\/$ $\/$

Colors of variables: wff set class

Syntax hints:

wn 3

wi 4 $/\$ wa 97

wb 98 $\/$ wo 628 DECID wdc 741

This theorem was proved from axioms: ax-1 5 ax-2 6 ax-mp 7 ax-ia1 99 ax-ia2 100 ax-ia3 101 ax-in1 544 ax-in2 545 ax-io 629

This theorem depends on definitions: df-bi 110 df-dc 742

This theorem is referenced by: (None)

W3C validator