Theorem peircedc 899

Description: Peirce's theorem for a decidable proposition. This odd-looking theorem can be seen as an alternative to exmiddc 821, condc 838, or notnotrdc 828 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 820	. 2 |- (DECID ph <-> ( ph \/ -. ph ) )
2		ax-1 6	. . 3 |- ( ph -> ( ( ( ph -> ps ) -> ph ) -> ph ) )
3		pm2.21 606	. . . . 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 705	. 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 697  DECID wdc 819

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 604  ax-io 698

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

This theorem is referenced by:  looinvdc  900  exmoeudc  2060