pm4.55dc - Intuitionistic Logic Explorer

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

Theorem pm4.55dc 928

Description: Theorem *4.55 of [WhiteheadRussell] p. 120, for decidable propositions. (Contributed by Jim Kingdon, 2-May-2018.)

**Assertion**
Ref	Expression
pm4.55dc	DECID DECID $/\$ $\/$

**Proof of Theorem pm4.55dc**
Step	Hyp	Ref	Expression
1		pm4.54dc 892	. . . . 5 DECID DECID $/\$ $\/$
2	1	imp 123	. . . 4 DECID $/\$ DECID $/\$ $\/$
3		dcn 832	. . . . . . . . 9 DECID DECID
4	3	anim2i 340	. . . . . . . 8 DECID $/\$ DECID DECID $/\$ DECID
5		dcor 925	. . . . . . . . 9 DECID DECID DECID $\/$
6	5	imp 123	. . . . . . . 8 DECID $/\$ DECID DECID $\/$
7	4, 6	syl 14	. . . . . . 7 DECID $/\$ DECID DECID $\/$
8		dcn 832	. . . . . . . . 9 DECID DECID
9		dcan2 924	. . . . . . . . 9 DECID DECID DECID $/\$
10	8, 9	syl 14	. . . . . . . 8 DECID DECID DECID $/\$
11	10	imp 123	. . . . . . 7 DECID $/\$ DECID DECID $/\$
12	7, 11	jca 304	. . . . . 6 DECID $/\$ DECID DECID $\/$ $/\$ DECID $/\$
13		con2bidc 865	. . . . . . 7 DECID $\/$ DECID $/\$ $\/$ $/\$ $/\$ $\/$
14	13	imp 123	. . . . . 6 DECID $\/$ $/\$ DECID $/\$ $\/$ $/\$ $/\$ $\/$
15	12, 14	syl 14	. . . . 5 DECID $/\$ DECID $\/$ $/\$ $/\$ $\/$
16	15	biimprd 157	. . . 4 DECID $/\$ DECID $/\$ $\/$ $\/$ $/\$
17	2, 16	mpd 13	. . 3 DECID $/\$ DECID $\/$ $/\$
18	17	bicomd 140	. 2 DECID $/\$ DECID $/\$ $\/$
19	18	ex 114	1 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)