Theorem peircedc 909

Description: Peirce's theorem for a decidable proposition. This odd-looking theorem can be seen as an alternative to exmiddc 831, condc 848, or notnotrdc 838 in the sense of expressing the "difference" between an intuitionistic system of propositional calculus and a classical system. In intuitionistic logic, it only holds for decidable propositions. (Contributed by Jim Kingdon, 3-Jul-2018.)

Assertion

Ref	Expression
peircedc	|- (DECID ph -> ( ( ( ph -> ps ) -> ph ) -> ph ) )

Proof of Theorem peircedc

Step	Hyp	Ref	Expression
1		df-dc 830	. 2 |- (DECID ph <-> ( ph \/ -. ph ) )
2		ax-1 6	. . 3 |- ( ph -> ( ( ( ph -> ps ) -> ph ) -> ph ) )
3		pm2.21 612	. . . . 5 |- ( -. ph -> ( ph -> ps ) )
4	3	imim1i 60	. . . 4 |- ( ( ( ph -> ps ) -> ph ) -> ( -. ph -> ph ) )
5	4	com12 30	. . 3 |- ( -. ph -> ( ( ( ph -> ps ) -> ph ) -> ph ) )
6	2, 5	jaoi 711	. 2 |- ( ( ph \/ -. ph ) -> ( ( ( ph -> ps ) -> ph ) -> ph ) )
7	1, 6	sylbi 120	1 |- (DECID ph -> ( ( ( ph -> ps ) -> ph ) -> ph ) )

Syntax hints:   -. wn 3   -> wi 4   \/ wo 703  DECID wdc 829

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-in2 610  ax-io 704

This theorem depends on definitions:  df-bi 116  df-dc 830

This theorem is referenced by:  looinvdc  910  exmoeudc  2082