dn1dc - Intuitionistic Logic Explorer

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

Theorem dn1dc 901

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 689	. . . . 5 $\/$
2		imnan 656	. . . . 5 $\/$ $\/$ $/\$
3	1, 2	mpbi 143	. . . 4 $\/$ $/\$
4	3	biorfi 697	. . 3 $\/$ $\/$ $/\$
5		orcom 679	. . 3 $\/$ $\/$ $/\$ $\/$ $/\$ $\/$
6		ordir 763	. . 3 $\/$ $/\$ $\/$ $\/$ $\/$ $/\$ $\/$
7	4, 5, 6	3bitri 204	. 2 $\/$ $\/$ $/\$ $\/$
8		pm4.45 730	. . . . . 6 $/\$ $\/$
9		simprrl 505	. . . . . . 7 DECID $/\$ DECID $/\$ DECID $/\$ DECID DECID
10		dcor 876	. . . . . . . . 9 DECID DECID DECID $\/$
11	10	imp 122	. . . . . . . 8 DECID $/\$ DECID DECID $\/$
12	11	ad2antll 474	. . . . . . 7 DECID $/\$ DECID $/\$ DECID $/\$ DECID DECID $\/$
13		anordc 897	. . . . . . 7 DECID DECID $\/$ $/\$ $\/$ $\/$ $\/$
14	9, 12, 13	sylc 61	. . . . . 6 DECID $/\$ DECID $/\$ DECID $/\$ DECID $/\$ $\/$ $\/$ $\/$
15	8, 14	syl5bb 190	. . . . 5 DECID $/\$ DECID $/\$ DECID $/\$ DECID $\/$ $\/$
16	15	orbi2d 736	. . . 4 DECID $/\$ DECID $/\$ DECID $/\$ DECID $\/$ $\/$ $\/$ $\/$
17	16	anbi2d 451	. . 3 DECID $/\$ DECID $/\$ DECID $/\$ DECID $\/$ $\/$ $/\$ $\/$ $\/$ $\/$ $/\$ $\/$ $\/$ $\/$
18		dcor 876	. . . . . . . 8 DECID DECID DECID $\/$
19		dcn 779	. . . . . . . 8 DECID $\/$ DECID $\/$
20	18, 19	syl6 33	. . . . . . 7 DECID DECID DECID $\/$
21	20	imp 122	. . . . . 6 DECID $/\$ DECID DECID $\/$
22	21	adantrr 462	. . . . 5 DECID $/\$ DECID $/\$ DECID $/\$ DECID DECID $\/$
23		dcor 876	. . . . 5 DECID $\/$ DECID DECID $\/$ $\/$
24	22, 9, 23	sylc 61	. . . 4 DECID $/\$ DECID $/\$ DECID $/\$ DECID DECID $\/$ $\/$
25		dcn 779	. . . . . . . 8 DECID DECID
26	9, 25	syl 14	. . . . . . 7 DECID $/\$ DECID $/\$ DECID $/\$ DECID DECID
27		dcn 779	. . . . . . . 8 DECID $\/$ DECID $\/$
28	12, 27	syl 14	. . . . . . 7 DECID $/\$ DECID $/\$ DECID $/\$ DECID DECID $\/$
29		dcor 876	. . . . . . 7 DECID DECID $\/$ DECID $\/$ $\/$
30	26, 28, 29	sylc 61	. . . . . 6 DECID $/\$ DECID $/\$ DECID $/\$ DECID DECID $\/$ $\/$
31		dcn 779	. . . . . 6 DECID $\/$ $\/$ DECID $\/$ $\/$
32	30, 31	syl 14	. . . . 5 DECID $/\$ DECID $/\$ DECID $/\$ DECID DECID $\/$ $\/$
33		dcor 876	. . . . . 6 DECID DECID $\/$ $\/$ DECID $\/$ $\/$ $\/$
34	33	imp 122	. . . . 5 DECID $/\$ DECID $\/$ $\/$ DECID $\/$ $\/$ $\/$
35	32, 34	syldan 276	. . . 4 DECID $/\$ DECID $/\$ DECID $/\$ DECID DECID $\/$ $\/$ $\/$
36		anordc 897	. . . 4 DECID $\/$ $\/$ DECID $\/$ $\/$ $\/$ $\/$ $\/$ $/\$ $\/$ $\/$ $\/$ $\/$ $\/$ $\/$ $\/$ $\/$ $\/$
37	24, 35, 36	sylc 61	. . 3 DECID $/\$ DECID $/\$ DECID $/\$ DECID $\/$ $\/$ $/\$ $\/$ $\/$ $\/$ $\/$ $\/$ $\/$ $\/$ $\/$ $\/$
38	17, 37	bitrd 186	. 2 DECID $/\$ DECID $/\$ DECID $/\$ DECID $\/$ $\/$ $/\$ $\/$ $\/$ $\/$ $\/$ $\/$ $\/$ $\/$
39	7, 38	syl5rbb 191	1 DECID $/\$ DECID $/\$ DECID $/\$ DECID $\/$ $\/$ $\/$ $\/$ $\/$ $\/$

Colors of variables: wff set class

Syntax hints:

wn 3

wi 4 $/\$ wa 102

wb 103 $\/$ wo 661 DECID wdc 775

This theorem was proved from axioms: ax-1 5 ax-2 6 ax-mp 7 ax-ia1 104 ax-ia2 105 ax-ia3 106 ax-in1 576 ax-in2 577 ax-io 662

This theorem depends on definitions: df-bi 115 df-dc 776

This theorem is referenced by: (None)

W3C validator