dn1dc - Intuitionistic Logic Explorer

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

Theorem dn1dc 950

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 728	. . . . 5 $\/$
2		imnan 680	. . . . 5 $\/$ $\/$ $/\$
3	1, 2	mpbi 144	. . . 4 $\/$ $/\$
4	3	biorfi 736	. . 3 $\/$ $\/$ $/\$
5		orcom 718	. . 3 $\/$ $\/$ $/\$ $\/$ $/\$ $\/$
6		ordir 807	. . 3 $\/$ $/\$ $\/$ $\/$ $\/$ $/\$ $\/$
7	4, 5, 6	3bitri 205	. 2 $\/$ $\/$ $/\$ $\/$
8		pm4.45 774	. . . . . 6 $/\$ $\/$
9		simprrl 529	. . . . . . 7 DECID $/\$ DECID $/\$ DECID $/\$ DECID DECID
10		dcor 925	. . . . . . . . 9 DECID DECID DECID $\/$
11	10	imp 123	. . . . . . . 8 DECID $/\$ DECID DECID $\/$
12	11	ad2antll 483	. . . . . . 7 DECID $/\$ DECID $/\$ DECID $/\$ DECID DECID $\/$
13		anordc 946	. . . . . . 7 DECID DECID $\/$ $/\$ $\/$ $\/$ $\/$
14	9, 12, 13	sylc 62	. . . . . 6 DECID $/\$ DECID $/\$ DECID $/\$ DECID $/\$ $\/$ $\/$ $\/$
15	8, 14	syl5bb 191	. . . . 5 DECID $/\$ DECID $/\$ DECID $/\$ DECID $\/$ $\/$
16	15	orbi2d 780	. . . 4 DECID $/\$ DECID $/\$ DECID $/\$ DECID $\/$ $\/$ $\/$ $\/$
17	16	anbi2d 460	. . 3 DECID $/\$ DECID $/\$ DECID $/\$ DECID $\/$ $\/$ $/\$ $\/$ $\/$ $\/$ $/\$ $\/$ $\/$ $\/$
18		dcor 925	. . . . . . . 8 DECID DECID DECID $\/$
19		dcn 832	. . . . . . . 8 DECID $\/$ DECID $\/$
20	18, 19	syl6 33	. . . . . . 7 DECID DECID DECID $\/$
21	20	imp 123	. . . . . 6 DECID $/\$ DECID DECID $\/$
22	21	adantrr 471	. . . . 5 DECID $/\$ DECID $/\$ DECID $/\$ DECID DECID $\/$
23		dcor 925	. . . . 5 DECID $\/$ DECID DECID $\/$ $\/$
24	22, 9, 23	sylc 62	. . . 4 DECID $/\$ DECID $/\$ DECID $/\$ DECID DECID $\/$ $\/$
25		dcn 832	. . . . . . . 8 DECID DECID
26	9, 25	syl 14	. . . . . . 7 DECID $/\$ DECID $/\$ DECID $/\$ DECID DECID
27		dcn 832	. . . . . . . 8 DECID $\/$ DECID $\/$
28	12, 27	syl 14	. . . . . . 7 DECID $/\$ DECID $/\$ DECID $/\$ DECID DECID $\/$
29		dcor 925	. . . . . . 7 DECID DECID $\/$ DECID $\/$ $\/$
30	26, 28, 29	sylc 62	. . . . . 6 DECID $/\$ DECID $/\$ DECID $/\$ DECID DECID $\/$ $\/$
31		dcn 832	. . . . . 6 DECID $\/$ $\/$ DECID $\/$ $\/$
32	30, 31	syl 14	. . . . 5 DECID $/\$ DECID $/\$ DECID $/\$ DECID DECID $\/$ $\/$
33		dcor 925	. . . . . 6 DECID DECID $\/$ $\/$ DECID $\/$ $\/$ $\/$
34	33	imp 123	. . . . 5 DECID $/\$ DECID $\/$ $\/$ DECID $\/$ $\/$ $\/$
35	32, 34	syldan 280	. . . 4 DECID $/\$ DECID $/\$ DECID $/\$ DECID DECID $\/$ $\/$ $\/$
36		anordc 946	. . . 4 DECID $\/$ $\/$ DECID $\/$ $\/$ $\/$ $\/$ $\/$ $/\$ $\/$ $\/$ $\/$ $\/$ $\/$ $\/$ $\/$ $\/$ $\/$
37	24, 35, 36	sylc 62	. . 3 DECID $/\$ DECID $/\$ DECID $/\$ DECID $\/$ $\/$ $/\$ $\/$ $\/$ $\/$ $\/$ $\/$ $\/$ $\/$ $\/$ $\/$
38	17, 37	bitrd 187	. 2 DECID $/\$ DECID $/\$ DECID $/\$ DECID $\/$ $\/$ $/\$ $\/$ $\/$ $\/$ $\/$ $\/$ $\/$ $\/$
39	7, 38	bitr2id 192	1 DECID $/\$ DECID $/\$ DECID $/\$ DECID $\/$ $\/$ $\/$ $\/$ $\/$ $\/$

Colors of variables: wff set class

Syntax hints:

wn 3

wi 4 $/\$ wa 103

wb 104 $\/$ wo 698 DECID wdc 824

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 604 ax-in2 605 ax-io 699

This theorem depends on definitions: df-bi 116 df-stab 821 df-dc 825

This theorem is referenced by: (None)

W3C validator